DAGSTUHL
2001
14 years 8 days ago
2001
We give two finite axiomatizations of indexed inductive-recursive definitions in intuitionistic type theory. They extend our previous finite axiomatizations of inductive-recursive...
TPHOL
2009
IEEE
14 years 5 months ago
2009
IEEE
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...
PLPV
2009
ACM
14 years 7 months ago
2009
ACM
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...