Research Proposals

Contact person: Andrés Sicard Ramírez

Statistical Methods and Automated Softwate Testing

Proposal date: 2017-03-04

Status: Open

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

Slides: [ pdf ]

Combining Interactive and Automatic Proofs (Apia)

Introduction

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:

References:

Apia: Connection to SMT Solvers

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:

Link: Haskell bindings for the Z3 SMT solver

Apia: Proof Reconstruction in Agda

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:

Link: SMTCoq

Apia: Web Interface for the ATPs

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.

Apia: Connection to Inductive Theorem Provers

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

First-Order Theory of Combinators (FOTC)

Introduction

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:

References:

FOTC: Polymorphism

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.

FOTC: Haskell Type Classes

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:

FOTC: Using Agda’s Standard Library for Proofs in FOTC

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:

FOTC: A Translator of Haskell Programs into FOTC Programs

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:

FOTC: Using Agda Combinators for Co-Induction

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 2.9.1.1.

Andrés Sicard Ramírez

Last modified: Sun Jan 19 18:30:46 -05 2020

Valid XHTML 1.0 Transitional