Author name cluster

André Hirschowitz

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

FSCD Conference 2020 Conference Paper

Modules over Monads and Operational Semantics

André Hirschowitz
Tom Hirschowitz
Ambroise Lafont

This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al. , we introduce transition monads, thus covering new applications such as ̅λμ-calculus, π-calculus, Positive GSOS specifications, differential λ-calculus, and the big-step, simply-typed, call-by-value λ-calculus. Finally, we design a suitable notion of signature for transition monads.

Details

CSL Conference 2018 Conference Paper

High-Level Signatures and Initial Semantics

Benedikt Ahrens
André Hirschowitz
Ambroise Lafont
Marco Maggesi

We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we consider a general notion of "signature" for specifying syntactic constructions. Our signatures subsume classical algebraic signatures (i. e. , signatures for languages with variable binding, such as the pure lambda calculus) and extend to much more general examples. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object - if it exists - in a suitable category of models. Our notions of signature and syntax are suited for compositionality and provide, beyond the desired algebra of terms, a well-behaved substitution and the associated inductive/recursive principles. Our signatures are "general" in the sense that the existence of an associated syntax is not automatically guaranteed. In this work, we identify a large and simple class of signatures which do generate a syntax. This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu. The main results presented in the paper are computer-checked within the UniMath system.

Details

I&C Journal 2010 Journal Article

Modules over monads and initial semantics

André Hirschowitz
Marco Maggesi

Inspired by the classical theory of modules over a monoid, we introduce the natural notion of module over a monad. The associated notion of morphism of left modules (“linear” natural transformations) captures an important property of compatibility with substitution, not only in the so-called homogeneous case but also in the heterogeneous case where “terms” and variables therein could be of different types. In this paper, we present basic constructions of modules and we show how modules allow a new point of view concerning higher-order syntax and semantics.

Details DOI

LPAR Conference 1994 Conference Paper

Higher-Order Abstract Syntax with Induction in Coq

Joëlle Despeyroux
André Hirschowitz

Abstract Three important properties of Higher-Order Abstract Syntax are the (higher-order) induction principle, which allows proofs by induction, the (higher-order) injection principle, which asserts that equal terms have equal heads and equal sons, and the extensionality principle, which asserts that functional terms which are pointwise equal are equal. Higher-order abstract syntax is implemented for instance in the Edinburgh Logical Framework and the above principles are satisfied by this implementation. But although they can be proved at the meta level, they cannot be proved at the object level and furthermore, it is not so easy to know how to formulate them in a simple way at the object level. We explain here how Second-Order Abstract Syntax can be implemented in a more powerful type system (Coq) in such a way as to make available or provable (at the object level) the corresponding induction, injection and extensionality principles.

Details