Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory (2009)
Andreas Abel, Thierry Coqu, Peter Dybjer
Abstract. Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of...
fax:+46 31 165655
Verifying haskell pro-grams by combining testing and proving (2008)
Peter Dybjer, Qiao Haiyan, Makoto Takeyama
We propose a method for improving confidence in the correctness of Haskell programs by combining testing and proving. Testing is used for debugging programs and specification before a costly proof...
Dependent Types at Work Lecture Notes for the LerNet Summer School (2008)
Abstract. In these lecture notes we give an introduction to functional programming with dependent types. We use the dependently typed programming language Agda which is based on ideas in Martin-Löf...
Dependent Types at Work Lecture Notes for the LerNet Summer School (2008)
Abstract. In these lecture notes we give an introduction to functional programming with dependent types. We use the dependently typed programming language Agda which is based on ideas in Martin-Löf...
Verifying a semantic βη-conversion test for Martin-Löf type theory (2008)
Andreas Abel, Thierry Coqu, Peter Dybjer
Abstract. Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of...
Inductive Definitions and Type Theory: An Introduction (2007)
Martin-Lof's type theory can be described as an intuitionistic theory of iterated inductive definitions developed in a framework of dependent types. It was originally intended to be a full-scale...
Variable Set Semantics for Predicate Logic and Problems of Semantic Database Theory (2007)
Zinovy Diskin, Professors Thierry Coqu, Peter Dybjer
lear that it should be a version of the hyperdoctrine construction, a well known categorical counterpart of predicate logic; ffl to understand this structure from the proof-theoretical and...
Abstract. We give two nite axiomatizations of indexed inductive-recursive de nitions in intuitionistic type theory. They extend our previous nite axiomatizations of inductive-recursive denitions of...
Peter Dybjer, Andrzej Filinski
Abstract. We give an introduction to normalization by evaluation and type-directed partial evaluation. We rst present normalization by evaluation for a combinatory version of Godel System T. Then we...
Normalization by evaluation for Martin-Löf type theory with one universe (2007)
Andreas Abel, Klaus Aehlig, Peter Dybjer, Abel Aehlig Dybjer
Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be
Normalization by evaluation for Martin-Löf type theory with one universe (2007)
Andreas Abel, Klaus Aehlig, Peter Dybjer, Abel Aehlig Dybjer
Replace this file with prentcsmacro.sty for your meeting, or with entcsmacro.sty for your meeting. Both can be
Formalizing categorical models of type theory in type theory (2007)
Alexandre Buisse, Peter Dybjer
This note is about work in progress on the topic of “internal type theory ” where we investigate the internal formalization of the categorical metatheory of constructive type theory in (an...
Indexed Induction-Recursion (2004)
An indexed inductive definition (IIRD) is a simultaneous inductive definition of an indexed family of sets. An inductive-recursive definition (IRD) is a simultaneous inductive definition of a set and...
Induction-recursion and initial algebras (2003)
1 Introduction Induction-recursion is a powerful definition method in intuitionistic type theory in the sense of Scott ("Constructive Validity") [31] and Martin-L"of [17,...
Universes for Generic Programs and Proofs in Dependent Type Theory (2003)
Marcin Benke, Peter Dybjer, Patrik Jansson
We show how to write generic programs and proofs in MartinL of type theory. To this end we consider several extensions of MartinL of's logical framework for dependent types. Each extension has a...
Combining Testing and Proving in Dependent Type Theory (2003)
Peter Dybjer, Qiao Haiyan, And Makoto Takeyama, Makoto Takeyama
We extend the proof assistant Agda/Alfa for dependent type theory with a modi ed version of Claessen and Hughes' tool QuickCheck for random testing of functional programs. In this way we combine...
Universes for Generic Programs and Proofs in Dependent Type Theory (2003)
Marcin Benke, Peter Dybjer, Patrik Jansson
We show how to write generic programs and proofs in MartinL of type theory. To this end we consider several extensions of MartinL of's logical framework for dependent types. Each extension has...
Normalization and partial evaluation (2002)
Peter Dybjer, Andrzej Filinski
Abstract. We give an introduction to normalization by evaluation and type-directed partial evaluation. We first present normalization by evaluation for a combinatory version of Gödel System T. Then...
Indexed induction-recursion (2001)
We give two finite axiomatizations of indexed inductive-recursive definitions in intuitionistic type theory. They extend our previous finite axiomatizations of inductive-recursive definitions of sets...
Normalization by Evaluation for Typed Lambda Calculus with Coproducts (2001)
Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip Scott, P. Scott
We solve the decision problem for simply typed lambda calculus with strong binary sums, equivalently the word problem for free cartesian closed categories with binary coproducts. Our method is based...
Indexed Induction-Recursion (2001)
Indexed induction-recursion is a principle for de ning new sets in Martin-Löf type theory. It extends the principle of induction-recursion to include the simultaneous inductive-recursive de nition...
Indexed Induction-Recursion (2001)
Peter Dybjer And, Peter Dybjer, Anton Setzer
We give two finite axiomatizations of indexed inductive-recursive definitions in intuitionistic type theory. They extend our previous finite axiomatizations of inductive-recursive definitions of sets...
Induction-Recursion and Initial Algebras (2000)
Induction-recursion is a powerful definition method in intuitionistic type theory. It extends (generalized) inductive definitions and allows us to define all standard sets of Martin-Lof type theory...
Induction-Recursion and Initial Algebras (2000)
Peter Dybjer And, Peter Dybjer, Anton Setzer
Induction-recursion is a powerful definition method in intuitionistic type theory. It extends (generalized) inductive definitions and allows us to define all standard sets of Martin-Lof type theory...
Induction-Recursion and Initial Algebras (2000)
Induction-recursion is a powerful definition method in intuitionistic type theory. It extends (generalized) inductive definitions and allows us to define all standard sets of Martin-Lof type theory...
A finite axiomatization of inductive-recursive definitions (1999)
Abstract Induction-recursion is a schema which formalizes the principles for introducing new sets in Martin-L"of's type theory. It states that we may inductively define a set while...
Intuitionistic Model Constructions and Normalization Proofs (1998)
We investigate semantical normalization proofs for typed combinatory logic and weak -calculus. One builds a model and a function `quote' which inverts the interpretation function. A...
A Finite Axiomatization of Inductive-Recursive Definitions (1998)
Peter Dybjer And, Peter Dybjer, Anton Setzer
Induction-recursion is a schema which formalizes the principles for introducing new sets in Martin-Lof's type theory. It states that we may inductively define a set while simultaneously defining...
Finite Axiomatizations of Inductive and Inductive-Recursive Definitions (1998)
We first present a finite axiomatization of strictly positive inductive types in the simply typed lambda calculus. Then we show how this axiomatization can be modified to encompass simultaneous...
A Finite Axiomatization of Inductive-Recursive Definitions (1998)
Induction-recursion is a schema which formalizes the principles for introducing new sets in Martin-Lof's type theory. It states that we may inductively define a set while simultaneously defining...
A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory (1998)
The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löf's universe à la Tarski. A set U0 of codes for small sets is generated inductively...
An ALF proof of Mac Lane's coherence theorem (1997)
A straightforward proof of the Coherence theorem for monoidal categories is presented in [2]. Here we describe the its formalisation within Martin-L#f type theory. The paper is organised as a...
A general formulation of inductive and recursive definitions in Martin-Lof's type theory is presented. It extends Backhouse's `Do-It-Yourself Type Theory' to include inductive...
A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem (1996)
Sten Agerholm, Ilya Beylin, Peter Dybjer
. We compare formalizations of an example from elementary category theory in the systems HOL (an implementation of Church's classical simple type theory) and ALF (an implementation of MartinL...
Intuitionistic Model Constructions and Normalization Proofs (1996)
The traditional notions of strong and weak normalization refer to properties of a binary reduction relation. In this paper we explore an alternative approach to normalization, where we bypass the...
. We introduce categories with families as a new notion of model for a basic framework of dependent types. This notion is close to ordinary syntax and yet has a clean categorical description. We also...
Representing Inductively Defined Sets by Wellorderings in Martin-Löf's Type Theory (1996)
We prove that every strictly positive endofunctor on the category of sets generated by Martin-Lof's extensional type theory has an initial algebra. This representation of inductively defined...
Abstract. This paper studies the problem of coherence in category theory from a type-theoretic viewpoint. We first show how a Curry-Howard interpretation of a formal proof of normalization for...
Ilya Beylin And, Ilya Beylin, Peter Dybjer
This paper studies a connection between intuitionistic type theory and coherence problems in the sense of category theory. We first show how a Curry-Howard interpretation of a formal proof of...
This paper studies the problem of coherence in category theory from a type-theoretic viewpoint. We first show how a Curry-Howard interpretation of a formal proof of normalization for monoids almost...
This paper studies a connection between intuitionistic type theory and coherence problems in the sense of category theory. We first show how a Curry-Howard interpretation of a formal proof of...
Inductive Definitions and Type Theory: An Introduction (1994)
this paper also the quite elegant case notation for the definition of functions over data types. He also discussed the general method of structural induction for proving properties of programs which...
On the Syntax of Dependent Types and the Coherence Problem (working draft) (1994)
We discuss different ways to represent the syntax of dependent types using Martin-Lof type theory as a metalanguage. In particular, we show how to give an intrinsic syntax in which meaningful...
Implementing a Category of Sets in ALF (1994)
Peter Dybjer And Veronica Gaspes, Peter Dybjer, Ver'onica Gaspes
Introduction Peter Aczel [1] and Gerard Huet [8] have implemented the category of sets in LEGO and Coq respectively. Here we show an implementation of the category of sets in ALF [2], a proof...
Inductive Sets and Families in Martin-Löf's Type Theory and Their Set-Theoretic Semantics (1991)
Martin-Lof's type theory is presented in several steps. The kernel is a dependently typed -calculus. Then there are schemata for inductive sets and families of sets and for primitive recursive...