Agda formalisation of FOTC (First-Order Theory of Combinators)

Description

Agda formalisation of FOTC (First-Order Theory of Combinators) which is a programming logic for functional programs that can deal with general recursion, higher-order functions, termination proofs, partial functions, and inductive and co-inductive predicates. Our implementation includes a translation of Agda representations of formulae in FOTC into the TPTP language, which is a standard format for input and output in automatic theorem provers (ATPs), so that we can call off-the-shelf ATPs when proving properties of our programs. For this purpose we wrote the Apia program.

Related publications

• Andrés Sicard-Ramírez (2015). Reasoning about Functional Programs by Combining Interactive and Automatic Proofs (PhD thesis).

• Ana Bove, Peter Dybjer and Andrés Sicard-Ramírez. Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs (FoSSaCS 2012).

• Ana Bove, Peter Dybjer and Andrés Sicard-Ramírez. Embedding a Logical Theory of Constructions in Agda (PLPV'09).

Prerequisites and use

• The Apia program

• Setting up the Emacs mode for use with our library of first-order theories

  It is necessary to add the path fotc/src/fot.

Examples in our FoSSaCS-2012 paper

Please note that the code presented here does not match the paper exactly.

You can follow these links to see the examples shown in our FoSSaCS-2012 paper:

• The McCarthy's 91-function example

• The mirror function example

• The alternating bit protocol example

You can test for example the proofs regarding the mirror function with the following commands:

$ cd fotc/src/fot
$ agda FOTC/Program/Mirror/PropertiesATP.agda
$ apia FOTC/Program/Mirror/PropertiesATP.agda

Examples in our PLPV-2009 paper

Please note that the code presented here does not match the paper exactly. Also note that the code below does not require neither the version modified of Agda nor the Apia program.

You can follow this link to see the examples shown in our PLPV-2009 paper.

You can test for example the verification of the GCD algorithm with the following commands:

$ cd fotc/src/fot
$ agda LTC-PCF/Program/GCD/Partial/CorrectnessProof.agda

More examples

We also have more examples related with first-order theories like group theory or Peano arithmetic. In addition there are more examples related to the verification of functional programs. You can browse all the examples from the file README.html.

Tested with

The files in this repository have been tested with:

Agda files: Development versions of the extended version of Agda, Apia and the Agda standard library.

Coq files: Coq 8.8.2

Haskell files: GHC 8.4.3