1 λ-calculus: Syntax and Computation strategies 7 1.1 Abstract syntax...................................... 7 1.2 Concrete syntax: pure λ-expressions.......................... 9
Abstract An analysis of Böhm’s theorem (2008)
We present in this article a detailed analysis of Böhm’s theorem, explained completely constructively as an algorithmic development in the functional language ML. 1
We present the Zen toolkit for morphological and phonological processing of natural languages. This toolkit is presented in literate programming style, in the Pidgin ML subset of the Objective Caml...
1 Automates Automates et machines (2008)
Soit S = 〈S, ·, 1 〉 un monoïde de support un ensemble S d’éléments appelés actions, muni d’une opération associative notée · appelée produit et d’un élément 1 neutre à gauche et...
The reactive engine for modular transducers (2005)
Abstract. This paper explains the design of the second release of the Zen toolkit [5–7]. It presents a notion of reactive engine which simulates finite-state machines represented as shared aums...
Abstract. We present a general methodology for non-deterministic programming based on pure functional programming. We construct families of automata constructions which are used as finite-state...
Abstract. Computational linguistics is an application of computer science which presents interesting challenges from the programming methodology point of view. Developing a realistic platform for the...
Linear Contexts and the Sharing Functor: Techniques for Symbolic Computation (2003)
We present in this paper two design issues concerning fundamental representation structures for symbolic and logic computations. The first one concerns structured editing, or more generally the...
Lexicon-directed Segmentation and Tagging of Sanskrit (2003)
We propose a methodology for Sanskrit processing by computer. The first layer of this software, which analyses the linear structure of a Sanskrit sentence as a set of possible interpretations under...
Towards Computational Processing of Sanskrit (2003)
We present in this paper recent progress in Sanskrit computational linguistics. We propose a solution to the tagging of verb phrases which correctly handles the non-associativity of external sandhi...
The Coq Proof Assistant : A Tutorial : Version 7.2 (2002)
Huet, Gérard, Kahn, Gilles, Paulin-Mohring, Christine
Coq is a proof assistant based on a higher-order logic. Coq allows to handle calculus mathematical assertions and to check mechanically proofs of these assertions. It helps to find formal proofs, and...
The Coq Proof Assistant : A Tutorial : Version 7.2 (2002)
Huet, Gérard, Kahn, Gilles, Paulin-Mohring, Christine
Coq is a proof assistant based on a higher-order logic. Coq allows to handle calculus mathematical assertions and to check mechanically proofs of these assertions. It helps to find formal proofs, and...
Constructive Category Theory (1998)
Gérard Huet, Amokrane Saïbi, Inria Rocquencourt
This paper give the full transcript of the Coq axiomatisation. In this note we develop one possible axiomatisation of the notion of category by modeling objects as types and Hom-sets as Hom-setoids...
The Coq Proof Assistant : A Tutorial : Version 6.1 (1997)
Huet, Gérard, Kahn, Gilles, Paulin-Mohring, Christine
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. This document is a tutorial for the version V6.1 of Coq. This version is available by anonymous ftp...
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
The Coq Proof Assistant : A Tutorial : Version 6.1 (1997)
Huet, Gérard, Kahn, Gilles, Paulin-Mohring, Christine
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. This document is a tutorial for the version V6.1 of Coq. This version is available by anonymous ftp...
The Coq Proof Assistant Reference Manual : Version 6.1 (1997)
Barras, Bruno, Boutin, Samuel, Cornes, Cristina, Courant, Judicaël, Filliâtre, Jean-Christophe, Giménez, Eduardo, ...
Coq is a proof assistant based on a higher-order logic allowing powerful definitions of functions. Coq V6.1 is available by anonymous ftp at ftp.inria.fr:/INRIA/Projects/coq/V6.1 and...
Finite-state Transducers as Regular Böhm Trees (1997)
Abstract. We present a uniform translation from finite-state transducers to regular Böhm trees presentations. The corresponding Böhm tree represents directly the trace semantics of all finite and...
Functional Pearl: The Zipper (1997)
Gérard Huet, Inria Rocquencourt France
Almost every programmer has faced the problem of representing a tree together with a subtree that is the focus of attention, where that focus may move left, right, up or down the tree. The Zipper is...
We give a decision procedure for the extensional equality of total Böhm trees presented by regular systems of recursion equations. 1. Böhm trees presentations Böhm trees are the natural infinite...
Specifications, Algorithms, Axiomatisations and Proofs Commented Case Studies (1995)
1.1 An overview of the specification language Gallina.................... 5
The Coq Proof Assistant - Reference Manual V 5.10 (1995)
Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Gérard Huet, Chetan Murthy, César Muñoz, ...
ion All Axiom Begin Cd Chapter Check CheckGuard CoFixpoint Compute Defined Definition Drop Elimination End Eval Explain Extraction Fact Fixpoint Focus for Go Goal Hint Hypothesis Immediate Induction...
Residual theory in λ-calculus: A formal development (1994)
Gérard Huet, Inria Rocquencourt
Abstract. We present the complete development, in Gallina, of the residual theory of β-reduction in pure λ-calculus. The main result is the Prism Theorem, and its corollary Lévy’s Cube Lemma, a...
An Analysis of Bohm's theorem (1993)
We present in this article a detailed analysis of Bhm's theorem, an essentialy separability results in pure l-calculus. The theorem is explained completely constructively as an algorithmic...
Residual theory in lambda-calculus : a formal development (1993)
We present the complete development, in Gallina, of the residual theory of b-reduction in pure l-calculus. The main result is the prism theorem and its corollary Levy's cube lemma, a strong form the...
An Analysis of Bohm's theorem (1993)
We present in this article a detailed analysis of Bhm's theorem, an essentialy separability results in pure l-calculus. The theorem is explained completely constructively as an algorithmic...
Residual theory in lambda-calculus : a formal development (1993)
We present the complete development, in Gallina, of the residual theory of b-reduction in pure l-calculus. The main result is the prism theorem and its corollary Levy's cube lemma, a strong form the...
Résumé disponible dans le fichier PDF
Résumé disponible dans le fichier PDF
Introduction ' Sri Yantra (also written Shri Yantra) is a sacred diagram of Tantric Hindhuism. Its symbolism is explained in Zimmer[15]. It consists in three concentric parts: ffl An inner...
Induction principles formalized in the Calculus of Constructions (1988)
The Calculus of Constructions is a higher-order formalism for writing constructive proofs in a natural deduction style, inspired from work of de Bruijn [2, 3], Girard [12], Martin-Löf [14] and Scott...