Sciweavers

Share
DAGSTUHL
2001
8 years 8 months ago
Indexed Induction-Recursion
We give two finite axiomatizations of indexed inductive-recursive definitions in intuitionistic type theory. They extend our previous finite axiomatizations of inductive-recursive...
Peter Dybjer, Anton Setzer
TPHOL
2009
IEEE
9 years 2 months ago
A Brief Overview of Agda - A Functional Language with Dependent Types
Abstract. We give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based on Martin-L¨of’s intuitionistic t...
Ana Bove, Peter Dybjer, Ulf Norell
PLPV
2009
ACM
9 years 4 months ago
Embedding a logical theory of constructions in Agda
We propose a new way to reason about general recursive functional programs in the dependently typed programming language Agda, which is based on Martin-L¨of’s intuitionistic ty...
Ana Bove, Peter Dybjer, Andrés Sicard-Ram&i...
books