A Tutorial on Recursive Types in Coq (1998)
This document is an introduction to the definition and use of recursive types in the Coq proof environment. It explains how recursive types like natural numbers and infinite streams are defined in...
A Tutorial on Recursive Types in Coq (1998)
This document is an introduction to the definition and use of recursive types in the Coq proof environment. It explains how recursive types like natural numbers and infinite streams are defined in...
A Tutorial on Recursive Types in Coq (1998)
This document is an introduction to the definition and use of recursive types in the Coq proof environment. It explains how recursive types like natural numbers and infinite streams are defined in...
Eduardo Giménez, Pierre Castéran
This document 1 is an introduction to the definition and use of inductive and co-inductive types in the Coq proof environment. It explains how types like natural numbers and infinite streams are...
A Tutorial on [Co-]Inductive Types in Coq (1998)
Eduardo Giménez, Pierre Castéran
This document 1 is an introduction to the definition and use of inductive and co-inductive types in the Coq proof environment. It explains how types like natural numbers and infinite streams are...
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 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 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...
Type Theory and Functional Programming: a work proposal (1997)
Gustavo Betarte, Ana Bove, Juan José Cabezas, Guillermo Calderón, Cristina Cornes, Sylvia Da Rosa, ...
We propose a series of work areas related to program verification, type theory and functional programming. The areas presented are: the implementation of an environment for carrying out constructions...
A Tutorial on Recursive Types in Coq (1996)
Contents 1 Recursive Types and Case Analysis 2 1.1 The predecessor function : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 1.2 The empty type : : : : : : : : : : : : : : : : :...
Experiences with a mechanisation of Martin-Löf's Theory of Types (1992)
Gustavo Betarte, Eduardo Giménez
Martin-Lof's Theory of Types-MLTT- can be used as a logical framework in which other theories can be defined. This paper describes ILF, a mechanisation of MLTT which allows definition of object...
On the positive fundamental value of money with short-sale constraints
Money, Short-sale constraints, Fundamental value, Asset pricing bubbles, (Technically) incomplete financial markets, Financial recognizability and insurance services, D52, E41, G12,