Paper Info
Title
Embedding a logical theory of constructions in Agda
Abstract
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öf's intuitionistic type theory. We show how to embed an external programming logic, Aczel's Logical Theory of Constructions (LTC) inside Agda. To this end we postulate the existence of a domain of untyped functional programs and the conversion rules for these programs. Furthermore, we represent the inductive notions in LTC (intuitionistic predicate logic with equality, and totality predicates) as inductive notions in Agda. To illustrate our approach we specify an LTC-style logic for PCF, and show how to prove the termination and correctness of a general recursive algorithm for computing the greatest common divisor of two numbers.
Year
DOI
Venue
2009
10.1145/1481848.1481857
PLPV
Keywords
Field
DocType
ltc-style logic,inductive notion,external programming logic,general recursive functional program,general recursive algorithm,logical theory,intuitionistic type theory,untyped functional program,programming language agda,intuitionistic predicate logic,recursive algorithm,functional programming,greatest common divisor,programming language,dependent types,type theory
Intuitionistic type theory,Programming language,Computer science,Correctness,Type theory,Algorithm,Termination analysis,Agda,Logic programming,Dependent type,Predicate logic
Conference
Citations 
PageRank 
References 
3
0.39
18
Authors
3
Name
Order
Citations
PageRank
Ana Bove119814.43
Peter Dybjer254076.99
Andrés Sicard-Ramírez360.78