HIGHER-ORDER ABSTRACT SYNTAX IN TYPE THEORY (2009)
Abstract. We develop a general tool to formalize and reason about languages expressed using higher-order abstract syntax in a proof-tool based on type theory (Coq). A language is specified by its...
Corecursive Algebras: A Study of General Structured Corecursion (Extended Abstract) (2009)
Venanzio Capretta, Tarmo Uustalu, Varmo Vene
Abstract. We study general structured corecursion, dualizing the work of Osius, Taylor, and others on general structured recursion. We call an algebra of a functor corecursive if it supports general...
COMMON KNOWLEDGE AS A COINDUCTIVE MODALITY (2009)
Abstract. I prove in Coq Aumann’s Theorem: In perfect information games, common knowledge of rationality implies backward induction equilibrium. The notion of common knowledge is formalized, using...
A Type of Partial Recursive Functions (2009)
Abstract. Our goal is to define a type of partial recursive functions in constructive type theory. In a series of previous articles, we studied two different formulations of partial functions and...
Higher Order Abstract Syntax in Type Theory (2008)
Venanzio Capretta, Amy P. Felty
We develop a general tool to formalize higher-order languages and reason about them in a proof-tool based on type theory (Coq). A language is specified by its signature, which consists of sets of...
Privacy in Data Mining Using Formal Methods (2008)
Stan Matwin, Amy Felty, István Hernádvölgyi, Venanzio Capretta
Abstract. There is growing public concern about personal data collected by both private and public sectors. People have very little control over what kinds of data are stored and how such data is...
Computation by Prophecy (2008)
Abstract. We describe a new method to represent (partial) recursive functions in type theory. For every recursive definition, we define a co-inductive type of prophecies that characterises the traces...
We describe the formalization of a correctness proof for a conflict detection algorithm for firewalls in the Coq Proof Assistant. First, we give formal definitions in Coq of a firewall access rule...
DOI: 10.1017/S0956796802004501 Printed in the United Kingdom Setoids in type theory (2008)
Gilles Barthe, Venanzio Capretta
Formalising mathematics in dependent type theory often requires to represent sets as setoids, i.e. types with an explicit equality relation. This paper surveys some possible definitions of setoids...
www.elsevier.com/locate/entcs Recursive Coalgebras from Comonads ⋆ 1,2 (2008)
Venanzio Capretta, Tarmo Uustalu, Varmo Vene
We discuss Osius’s [22] concept of a recursive coalgebra of a functor from the perspective of programming semantics and give some new sufficient conditions for the recursiveness of a...
We describe the formalization of a correctness proof for a conflict detection algorithm for firewalls in the Coq Proof Assistant. First, we give formal definitions in Coq of a firewall access rule...
Privacy in Data Mining Using Formal Methods (2008)
Stan Matwin, Amy Felty, István Hernádvölgyi, Venanzio Capretta
Abstract. There is growing public concern about personal data collected by both private and public sectors. People have very little control over what kinds of data are stored and how such data is...
Privacy in Data Mining Using Formal Methods (2008)
Stan Matwin, Amy Felty, István Hernádvölgyi, Venanzio Capretta
Abstract. There is growing public concern about personal data collected by both private and public sectors. People have very little control over what kinds of data are stored and how such data is...
The Logic and Mathematics of Occasion Sentences (2007)
Venanzio Capretta, Herman Geuvers
The prime purpose of this paper is to contribute to the development of an adequate logic of occasion sentences and a mathematical (Boolean) foundation for such a logic, thus preparing the ground for...
Equational Reasoning in Type Theory (2007)
Abstract. We dene the notions of equational theory and equational logic in Type Theory using the development of Universal Algebra presented in a previous paper. The main result is the formal proof of...
Gilles Barthe, Venanzio Capretta, Olivier Pons
Abstract. Formalising mathematics in dependent type theory often requires to use setoids, i.e. types with an explicit equality relation, as a representation of sets. This paper surveys some possible...
Gilles Barthe, Venanzio Capretta, Olivier Pons
Abstract. We show that two approaches commonly used to formalise sets in type theory, partial setoids and total setoids, are in fact not equivalent. More precisely, we show that total setoids form a
Recursive Families of Inductive Types (2007)
Abstract. Families of inductive types dened by recursion arise in the formalization of mathematical theories. An example is the family of term algebras on the type of signatures. Type theory does not...
Gilles Barthe, Venanzio Capretta, Olivier Pons
Abstract. Formalising mathematics in dependent type theory often requires to use setoids, i.e. types with an explicit equality relation, as a representation of sets. This paper surveys some possible...
Combining de Bruijn indices and higher-order abstract syntax in Coq (2006)
Venanzio Capretta, Amy P. Felty
Abstract. The use of higher-order abstract syntax is an important approach for the representation of binding constructs in encodings of languages and logics in a logical framework. Formal...
Combining de Bruijn indices and higher-order abstract syntax in Coq (2006)
Venanzio Capretta, Amy P. Felty
Abstract. The use of higher-order abstract syntax is an important approach for the representation of binding constructs in encodings of languages and logics in a logical framework. Formal...
General Recursion via Coinductive Types (2005)
A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the...
Recursive functions with higher order domains (2005)
Abstract. In a series of articles, we developed a method to translate general recursive functions written in a functional programming style into constructive type theory. Three problems remained: the...
Recursive Coalgebras from Comonads (2004)
Venanzio Capretta, Tarmo Uustalu, Varmo Vene
We discuss Osius's [22] concept of a recursive coalgebra of a functor from the perspective of programming semantics and give some new su#cient conditions for the recursiveness of a...
Modelling General Recursion in Type Theory (2004)
this paper is also included. A tutorial on the method can also be found in Bove 2003. Since our method separates the computational part from the logical part of a de nition, formalising partial...
Dybjer’s simultaneous inductive-recursive definitions [3] can be represented in the Calculus of Inductive Constructions by an impredicative Σ-type. The idea was suggested by the presentation of...
www.lmcs-online.org GENERAL RECURSION VIA COINDUCTIVE TYPES (2004)
Abstract. A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches...
Constructive type theory is an expressive programming language in which both algorithms and proofs can be represented. A limitation of constructive type theory as a programming language is that only...
Type-theoretic functional semantics (2002)
Yves Bertot, Venanzio Capretta, Kuntal Das Barman
Abstract. We describe the operational and denotational semantics of a small imperative language in type theory with inductive and recursive definitions. The operational semantics is given by natural...
Modelling General Recursion in Type Theory (2002)
Constructive type theory is an expressive programming language where both algorithms and proofs can be represented. However, general recursive algorithms have no direct formalisation in type theory...
Type-theoretic functional semantics (2002)
Yves Bertot, Venanzio Capretta, Kuntal Das Barman
Abstract. We describe the operational and denotational semantics of a small imperative language in type theory with inductive and recursive definitions. The operational semantics is given bynatural...
Abstraction and Computation: Type Theory, Algebraic Structures, and Recursive Functions (2002)
Venanzio Capretta, Venanzio Capretta, Dr. H. J. Geuvers, Prof Dr. Bart Jacobs
een wetenschappelijke proeve op het gebied van de Natuurwetenschappen, Wiskunde en Informatica Proefschrift ter verkrijging van de graad van doctor aan de Katholieke Universiteit Nijmegen, volgens...
Nested general recursion and partiality in type theory (2001)
Abstract. We extend Bove's technique for formalising simple general recursive algorithms in constructive type theory to nested recursive algorithms. The method consists in dening an inductive...
Nested general recursion and partiality in type theory (2001)
Abstract. We extend Bove’s technique for formalising simple general recursive algorithms in constructive type theory to nested recursive algorithms. The method consists in defining an inductive...
Certifying the fast Fourier transform with Coq (2001)
Abstract. We program the Fast Fourier Transform in type theory, using the tool Coq. We prove its correctness and the correctness of the Inverse Fourier Transform. A type of trees representing vectors...
Universal algebra in type theory (1999)
Abstract. We present a development of Universal Algebra inside Type Theory, formalized using the proof assistant Coq. We dene the notion of a signature and of an algebra over a signature. We use...
Universal algebra in type theory (1999)
Abstract. We present a development of Universal Algebra inside Type Theory, formalized using the proof assistant Coq. We define the notion of a signature and of an algebra over a signature. We use...
Venanzio Capretta, Silvio Valentini
and second order typed λ-calculi
Type-Theoretic Functional Semantics
Yves Bertot, Venanzio Capretta, Kuntal Das Barman
We describe the operational and denotational semantics of a small imperative language in type theory with inductive and recursive de nitions. The operational semantics is given by natural inference...