CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Embedding a Logical Theory of Constructions in Agda

Ana Bove (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; Peter Dybjer (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; Andres Sicard-Ramirez
Proceedings of the 2009 ACM SIGPLAN Workshop on Programming Languages meets Program Verification (PLPV) 2009 p. 59-66. (2009)
[Konferensbidrag, refereegranskat]

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.

Nyckelord: Logical theory of constructions, type theory, general recursion



Denna post skapades 2009-12-11. Senast ändrad 2015-02-11.
CPL Pubid: 103337

 

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)

Ämnesområden

Datalogi

Chalmers infrastruktur