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

Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs

Ana Bove (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; Peter Dybjer (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)) ; Andrés Sicard-Ramírez
Lecture Notes in Computer Science. 15th International Conference on Foundations of Software Science and Computational Structures, Tallinn, 24 March - 1 April 2012 (0302-9743). Vol. 7213 (2012), p. 104-118.
[Konferensbidrag, refereegranskat]

We propose a new approach to the computer-assisted verification of functional programs. We work in first order theories of functional programs which are obtained by extending Aczel's first order theory of combinatory formal arithmetic with positive inductive and coinductive predicates. Rather than building a special purpose system we implement our theories in Agda, a proof assistant for dependent type theory which can be used as a generic theorem prover. Agda provides support for interactive reasoning by encoding first order theories using the formulae-as-types principle. Further support is provided by off-the-shelf automatic theorem provers for first order logic which can be called by a program which translates Agda representations of first order formulae into the TPTP language understood by the provers. We show some examples where we combine interactive and automatic reasoning, covering both proof by induction and coinduction.



Denna post skapades 2012-06-19. Senast ändrad 2015-12-08.
CPL Pubid: 159212

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

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

Ämnesområden

Datalogi

Chalmers infrastruktur