**Proposal date:** 2017-03-04

**Status:** Open

**Authors:** Henry Laniado-Rodas and Andrés Sicard-Ramírez

**Slides:** [ .pdf ]

Apia is a Haskell program for proving first-order theorems written in the dependently typed language Agda using first-order automatic theorem provers (ATPs), via the translation of the Agda formulae to the TPTP format which is a standard for input and output for the ATPs.

**Source code:**

Apia program: Git repository apia

The file README.md contains the instructions for the installation.

**References:**

Haskell

Miran Lipovača (2011). Learn You a Haskell for Great Good!.

Bryan O'Sullivan, Don Stewart and John Goerzen (2008). Real World Haskell.

Agda

- Ana Bove and Peter Dybjer (2009). Dependent Types at Work. In: LerNet ALFA Summer School 2008. Ed. by A. Bove, L. Soares Barbosa,
- Pardo and J. Sousa Pinto. Vol. 5520. LNCS. Springer, pp. 57-99.

Ulf Norell (2009). Dependently Typed Programming in Agda. In: Advanced Functional Programming (AFP 2008). Ed. by P. Koopman, R. Plasmeijer and D. Swierstra. Vol. 5832. LNCS. Springer, pp. 230-266.

Apia

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 (2012). Combining interactive and automatic reasoning in first order theories of functional programs. FoSSaCS 2012.

**Proposal date:** 27 Nov. 2012

**Last modification:** 01 November 2015

**Status:** Work in progress. Research project by Andrés Sicard-Ramírez and Juan Fernando Ospina-Giraldo

We use our combined proof approach based on ATPs for proving (for example) some properties related to inequalities of natural numbers (see, for example, the proof of some arithmetic properties related to the verification of the McCarthy 91 function). However, we think that by using SMT solvers instead of ATPs, these kind of proofs would more automatics. In addition, there are systems like MetiTarski which is designed to prove universally quantified inequalities (in a certain theory), where the above kind of automatic proofs should be easier to prove. The proposal consists in the use of SMT solvers in our approach and to establish their relation to the ATPs.

**References:**

Clark Barret, Roberto Sebastiani, Sanjit A. Seshia and Cesare Tinelli. Satisfiability module theories (2009). In Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsh, editors. Handbook of Satisfiability. IOS Press, Chapter 26.

Pascal Fontaine et al. Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants (2006). In H. Hermanns and J. Palsberg (Eds.): TACAS 2006, LNCS 3920, pp. 167-181.

**Link:** Haskell bindings for the Z3 SMT solver

**Proposal date:** 2012-11-27

**Last modification:** 2017-03-04

**Status:** Work in progress by Jonathan Steven Prieto-Cubides and Andrés Sicard-Ramírez.

At the moment, the communication between Agda and the ATPs is one-directional. A first-order conjecture represented in Agda using our approach is sent to the ATPs via the Apia program, and the ATPs prove or disprove it (using a fixed timeout). To increase the reliability of our approach would be highly desirable to establish the communication in the other direction. The proposal consists in the construction of the Agda proof terms associated with the proved conjectures, from their ATP proofs.

**References:**

Jasmin Christian Blanchette. My Life with an Automatic Theorem Prover.

Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka and Albert Steckermeier. Semi-intelligible Isar Proofs from Machine-Generated Proofs. (Draft version).

Jasmin C. Blanchette and Cezary Kaliszyk and Lawrence C. Paulson (2014). Hammering towards QED. (Draft version).

Simon Foster and Georg Struth (2011). Integrating an automated theorem prover in Agda. In Bobaru et al., editors. NASA Formal Methods (NFM 2011), volume 6617 of LNCS, pages 116–130.

Böhme, Sascha and Weber, Tjark (2010). Fast LCF-Style Proof Reconstruction for Z3. In: Interactive Theorem Proving (ITP 2010). Ed. by Kaufmann, Matt and Paulson, Lawrence C. Vol. 6172. LNCS, pp. 179–194.

Pascal Fontaine et al (2006). Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. In H. Hermanns and J. Palsberg (Eds.): TACAS 2006, LNCS 3920, pp. 167-181.

Jia Meng, Claire Quigley and Lawrence C. Paulson (2006). Automation for interactive proof: First prototype. Information and computation, 204(10):1575–1596.

Marc Bezem, Dimitri Hendrinks and Hans de Nivelle (2002). Automated Proof Construction in Type Theory using Resolution.

**Link:** SMTCoq

**Proposal date:** 2012-11-27

**Last modification:** 2017-03-04

**Status:** Closed

The TPTP World offers an excellent web interface for many ATPs. This interface is called SystemOnTPTP. The proposal consists in the integration of this service with our Apia program, which would avoid the user needs to install the ATPs used in your proofs. The Sledgehammer tool for the Isabelle proof assistant uses this service.

Jonathan Steven Prieto-Cubides implements the online-atps command-line tool.

**Proposal date:** 27 Nov. 2012

**Last modification:** 01 April 2014

**Status:** Open

In FOTC we do not represent for example the natural numbers by an inductive set, but for an inductively defined predicate `N(t)`

whose axioms are `N(0)`

and `∀ t. N(t) → N(succ(t))`

, where `0`

and `succ`

are FOTC terms. By using the ATPs our inductive proofs on `N(t)`

using the following methodology: (i) we interactively instruct Agda to do pattern matching on the argument(s) that satisfy the inductive predicate and (ii) we automatically prove the base and step cases of the induction (see, for example, the proof that the addition of total natural numbers is a total natural number). By using inductive theorem provers we think that step (i) in the above methodology can be automated. The proposal consists in the use of inductive theorems provers in our approach.

**Link:** List of inductive theorem provers

The proposals here deal with *reasoning about functional programs by combining interactive and automatic proofs*. In joint work with Ana Bove and Peter Dybjer, we propose a new approach to the computer-assisted verification of *lazy* functional programs, where functions can be defined by *general* recursion. We work in a First-Order Theory of Combinators (FOTC) which can deal with general recursion, higher-order functions, termination proofs, and inductive and co-inductive definitions. Rather than building a special purpose system, we implement FOTC 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 (ATPs) which can be called by the Apia program, which translates our Agda representation of first-order formulae into the TPTP language understood by the ATPs.

**Source code:**

Extended version of Agda: Git repository eagda

Apia program: Git repository apia

Agda implementation of FOTC and some examples of verification of functional programs: Git repository fotc

The file README.md contains the instructions for the installation.

**References:**

Haskell

Miran Lipovača (2011). Learn You a Haskell for Great Good!.

Bryan O'Sullivan, Don Stewart and John Goerzen (2008). Real World Haskell.

Agda

- Ana Bove and Peter Dybjer (2009). Dependent Types at Work. In: LerNet ALFA Summer School 2008. Ed. by A. Bove, L. Soares Barbosa,
- Pardo and J. Sousa Pinto. Vol. 5520. LNCS. Springer, pp. 57-99.

Ulf Norell (2009). Dependently Typed Programming in Agda. In: Advanced Functional Programming (AFP 2008). Ed. by P. Koopman, R. Plasmeijer and D. Swierstra. Vol. 5832. LNCS. Springer, pp. 230-266.

First-order theory of combinators (FOTC)

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 (2012). Combining interactive and automatic reasoning in first order theories of functional programs. FoSSaCS 2012.

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

**Proposal date:** 18 Feb. 2013

**Status:** Open

Since FOTC is a type-free logic, for example, the inductive predicate `List`

represents ``heterogeneous'' total lists, such as

```
xs : D
xs = 0 ∷ true ∷ 1 ∷ false ∷ []
```

where the proof of its finiteness is given by

```
xs-List : List xs
xs-List = lcons 0 (lcons true (lcons 1 (lcons false lnil)))
```

We can also represent homogeneous total lists. For example, the total lists of total natural numbers are represented by the inductive predicate `ListN`

. An example of such lists and its proof of finiteness are given by

```
ys : D
ys = 0 ∷ 1 ∷ 2 ∷ []
```

```
ys-ListN : ListN ys
ys-ListN = lncons nzero (lncons (nsucc nzero) (lncons (nsucc (nsucc nzero)) lnnil)
```

Instead of representing total lists of terms satisfying a particular unary inductive predicate `P`

using a new list predicate, we can define an inductive predicate `Plist`

of polymorphic total lists parametrised by the predicate `P`

```
data Plist (P : D → Set) : D → Set where
lnil : Plist P []
lcons : ∀ {x xs} → P x → Plist P xs → Plist P (x ∷ xs)
```

By using the predicate `Plist`

, the ``heterogeneous'' total lists and the total lists of total natural numbers can be defined, respectively, by

```
List : D → Set
List = Plist (λ d → d ≡ d)
```

```
ListN : D → Set
ListN = Plist N
```

Unfortunately, this approach for representing polymorphic total lists is not within first-order logic, because we cannot use `P : D → Set`

as a parameter. In other words, `Plist (λ d → d ≡ d)`

and `Plist N`

are not first-order formulae. The previous discussion also applies to co-inductive types such as `Stream`

. The proposal consists in to represent, if it is possible, polymorphic total lists (or streams) in FOTC.

**Proposal date:** 18 Feb. 2013

**Status:** Open

Agda instance arguments can be used to model Haskell type classes (Devriese and Piessens 2011; Kettelhoit 2012). Based on the approach of Devriese and Piessens (2011), we shall try to represent the equality type class for the inductive predicates. We start by defining a record parametrised by a predicate `P : D → Set`

:

```
record Eq (P : D → Set) : Set₁ where
field equal : ∀ {t₁ t₂} → P t₁ → P t₂ → Set
```

Now, we can define for example, the `Bool`

and `N`

instances by

```
eqInstanceBool : Eq Bool
eqInstanceBool = record { equal = boolEq }
```

```
eqInstanceN : Eq N
eqInstanceN = record { equal = nEq }
```

where the functions `boolEq`

and `nEq`

are defined by

```
boolEq : ∀ {b₁ b₂} → Bool b₁ → Bool b₂ → Set
boolEq btrue btrue = Bool true
boolEq bfalse bfalse = Bool true
boolEq _ _ = Bool false
```

```
nEq : ∀ {m n} → N m → N n → Set
nEq nzero nzero = Bool true
nEq (nsucc Nm) (nsucc Nn) = Bool true
nEq _ _ = Bool false
```

Without going into the interesting details of the representation of Haskell type classes in Agda, this approach is not within FOL, because the record is of type `Set₁`

, that is, we would be talking about FOTC using universes. The proposal consists in to represent, if it is possible, type classes for the (co-)inductive predicates in FOTC.

**References:**

Dominique Devriese and Frank Piessens (2011). On the Bright Side of Type Classes: Instance Arguments in Agda. In: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (ICFP '11), pp. 143-155.

Frederic Kettelhoit (2012). Toward a Prelude for Agda. MA thesis. Institut für Informatik: Ludwig-Maximilians-Universität München.

**Proposal date:** 18 Feb. 2013

**Status:** Open

In FOTC, we use functions such as addition, multiplication and greater-than, among others. These functions are defined by structural recursion and will pass Agda's termination checker, so there is no need to leave a standard dependent type theory and move to FOTC to prove their properties. Moreover, they are basic functions, the properties of which can be expected to be found in a library as Agda's standard library. Based on the existence of a translation of Martin-Löf Type Theory into LTC (Aczel 1977; Smith 1978, 1984), the proposal consist in to transfer these kind of functions and the proofs of their properties to FOTC.

**References:**

Peter Aczel (1977). The Strength of MartinLöf's Intuitionistic Type Theory with One Universe. In: Proc. of the Symposium on Mathematical Logic (Oulu, 1974). Ed. by S. Miettinen and J. Väänanen. Report No. 2, Department of Philosophy, University of Helsinki, Helsinki, pp. 1-32.

Jan Smith (1978). On the relation between a Type Theoretic and a Logic Formulation of the Theory of Constructions. PhD thesis. Department of Mathematics: Chalmers University of Technology and University of Gothenburg.

Jan Smith (1984). An Interpretation of Martin-Löf's Type Theory in a Type-Free Theory of Propositions. In: The Journal of Symbolic Logic 49.3, pp. 730-753.

**Proposal date:** 18 Feb. 2013

**Last modification:** 20 Nov. 2013

**Status:** Open

At the moment, we manually translate Haskell programs into FOTC programs. Haskell is a huge language which is translated into a small strongly-typed core language by the GHC compiler (see, for example, Marlow and Peyton-Jones 2012). The proposal consists in to translate Haskell programs into FOTC programs.

**Related work:** Hip—the Haskell Inductive Prover—translates Haskell programs into first-order logic using an intermediate language (Rosén 2012). HALO translation is from GHC core to first-order logic (Vytiniotis, Peyton Jones, Claessen and Rosén 2012).

**References:**

Marlow, S. and Peyton-Jones, S. (2012). The Glasgow Haskell Compiler. In: The Architecture of Open Source Application. Volume II: Structure, Scale, and a Few More Fearless Hacks. Ed. by Brown, A. and Wilson, G. Amazon Digital Services, Inc.

Rosén, D. (2012). Proving Equational Haskell Properties Using Automated Theorem Provers. MA thesis. University of Gothenburg.

Vytiniotis, D., Peyton Jones, S., Rosén, D. and Claessen, K. (2013). HALO: Haskell to Logic thorugh Denotational Semantics. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’13), pp. 431–442.

**Proposal date:** 18 Feb. 2013

**Status:** Open

In FOTC, we define the co-inductive types by postulating their properties. For example, the co-inductive natural numbers are defined by the co-inductively defined predicate Conat together with its unfolding rule Conat-unf and its co-induction rule Conat-coind. The proposal consists in to use, if it is possible, Agda *non-first-order* combinators for co-induction, which are defined in the Agda's standard library (module Coinduction), to represent the FOTC co-inductive predicates in our approach.

Generated with pandoc 1.19.2.1

Last modified: Sat Mar 4 09:32:05 COT 2017