proj-plbook-plChProofLangs

Table of Contents for Programming Languages: a survey

Chapter : Proof assistant languages

Coq

Not Turing-complete (termination condition)

"Contemporary provers (built upon consistent Martin-Löf Type Theory, 1972) like Agda, Coq, Lean, F*, Idris are based on Barendregt and Coquand' CoC? with different flavors of infinity universe hierarchies and Calculus of Inductive Constructions. Some of them are automated and some are trying to be and general purpose programming languages with proving facilities." [1]

Links:

Agda

Not Turing-complete (termination condition) (sorta)

"Contemporary provers (built upon consistent Martin-Löf Type Theory, 1972) like Agda, Coq, Lean, F*, Idris are based on Barendregt and Coquand' CoC? with different flavors of infinity universe hierarchies and Calculus of Inductive Constructions. Some of them are automated and some are trying to be and general purpose programming languages with proving facilities." [2]

HOL

Succeeded by Isabelle.

Isabelle

ACL2

1996.

Not Turing-complete (termination condition)

Epigram

Not Turing-complete (termination condition)

Charity

Not Turing-complete (termination condition). Categorical semantics? [3]

Twelf

SPIN model checker and Promela

Some interesting constructs

'do' (do-od): a looping construct. Presumably loops until the command 'break' is executed. Like some forms of 'switch', it has multiple branches (delimited by '::'), and each branch has a guard (separated from the branch code by '->'). I think if multiple branch guards are True, then a non-deterministic choice is made. I think if all other branch guards are false, the 'else' guard is True.

bare expressions for blocking: when a bare expression, such as 'finish == 2', is encountered, the thread blocks until the expression returns True

'assert': assertions work as usual, but in addition, since Promela is a language for SPIN the model-checker, assertions are recognized by SPIN

'[]' is 'always': eg '[]!deadlock' means 'it is always true that deadlock is false'

'<>' is 'eventually': eg '[](request-resource -> <>granted-resource)' means 'always (if a resource is requested, eventually it is granted)'

Example

from http://spinroot.com/spin/Doc/p40-ben-ari.pdf (section 7):

byte n = 0, finish = 0;

active [2] proctype P() {
  byte register, counter = 0;
  do :: counter = 10 -> break
     :: else ->
             register = n;
             register++;
             n = register;
             counter++
  od;
  finish++
}

active proctype WaitForFinish() {
  finish == 2;
  printf(“n = %d\n”, n)
}

this is a program with two simultaneously executing threads with identical code ("active [2] proctype P()") and a third simultaneously executing thread ("active proctype WaitForFinish?()"). Each thread has access to two globals (n and finish) and two threadlocals (register and counter). Each thread effectively does a 'for' loop with 10 iterations; on each iteration it loads the current value of the global 'n' into threadlocal 'register', then increments 'register', then stores the result back into global 'n'. Before each thread terminates it (atomically, i presume) increments global 'finish'.

WaitForFinish? blocks until finish == 2, then prints out the value of global "n" to the console.

Links

Z3

MIT license.

ATS

Idris

NuPRL

Mizar

1989

Otter

1996

F*

"Contemporary provers (built upon consistent Martin-Löf Type Theory, 1972) like Agda, Coq, Lean, F*, Idris are based on Barendregt and Coquand' CoC? with different flavors of infinity universe hierarchies and Calculus of Inductive Constructions. Some of them are automated and some are trying to be and general purpose programming languages with proving facilities." [4]

LEAN

"Contemporary provers (built upon consistent Martin-Löf Type Theory, 1972) like Agda, Coq, Lean, F*, Idris are based on Barendregt and Coquand' CoC? with different flavors of infinity universe hierarchies and Calculus of Inductive Constructions. Some of them are automated and some are trying to be and general purpose programming languages with proving facilities." [5]

Links:

OM/EXE

Overview

http://groupoid.space/intro.htm speaks of untyped lambda calculus and LISP etc, and then ML ", founded merely on algebraic datatypes and algebra on higher terms rather than categorical semantic", and then ML being "fixed with categorical methods" in Charity etc, then HOL/Isabelle. It also mentions other 80s and 90s automated theory provers including Mizar, ACL2, Otter. It then says:

" MLTT

Contemporary provers (built upon consistent Martin-Löf Type Theory, 1972) like Agda, Coq, Lean, F*, Idris are based on Barendregt and Coquand' CoC? with different flavors of infinity universe hierarchies and Calculus of Inductive Constructions. Some of them are automated and some are trying to be and general purpose programming languages with proving facilities. "

and

lists Om/EXE's strengths as:

and the Github page describes it as:

"Groupoid Infinity creates a new programming language with dependent types called EXE with small provable dependent core called OM. OM is an implementation of Calculus of Constructions (CoC?), the pure lambda calculus with dependent types. It can be compiled (code extraction) to bytecode of Erlang virtual machines BEAM and LING. EXE is an implementation of Calculus of Inductive Constructions (CiC?) that lives on top of CoC? OM model. You may think of EXE as AST transformation of higher language (with HITs) to OM. "

the Github page also says:

" Technically it is useful to distinguish different layers of EXE:

    Internal Core with record used as structures, modules, and namespaces for the entire language. It transparently translates to OM as Contexts (named types and terms).
    Metaprogramming Encodings layer which allows expanding macros to Internal Core. Macros are used to encoding programming that hides implementation details of CPS, Parigot or Church encodings. However, our EXE encodings are a bit different encodings with categorical semantics, proven in Lean model.
    End-user Top-level EXE Language with powerful primitives data and codata that uses underlying encoding macros. In the future with inductive-inductive types and HITs. Likely Top Language would be a superset of the Internal Core sharing most of the parser."

OM/EXE language

toread: i think a lot of explanation is in here: https://github.com/groupoid/exe/blob/master/doc/proposal.pdf

https://github.com/groupoid/exe/blob/master/doc/encoding.pdf might also be of use but it looks advanced

[6] " DATE: 19 MAR 2016 Compiler Passes

Logic

Macros

Base Library

"

[7] (the following is mostly direct or paraphrased quotes from that page):

Core Types Inductive Dependent Base Library Exe Prelude

... N : Not a R : Recursive D : Dependent + : Inductive

todo my note: 'data' is listed as 'inductive' and 'record' is listed as 'coinductive'. E notes that 'sum' is related to the 'data' declaration. Perhaps 'inductive' and 'coinductive' are somehow related to sum and product types? in https://github.com/groupoid/exe/blob/master/doc/proposal.pdf section 'Inductive Types' it says that indeed "We extend the core PTS language with inductive data and coinductive record definitions" and "we call induction recursive sums" and "such kind of recursion on infinite lists (codata...coinductive types) we can call recursive products".

(constructors are listed below; then sometimes ';' followed by other comments)

todo ((?? not in main list on top, but listed under 'inductive' lower down:))

todo ((?? not in main list on top, but listed under 'logic' lower down:))

NR ND +

R ND +

NR D +

R D +

NR ND *

R ND *

NR D *

R D * todo * GROUPOID: ob, hom; 'hom' has a syntactically similar thingee as in SETOID, except that there's two implications instead of one, and at the right of the second is 'groupoid' (so i can't really interpret this the way i interpreted the rest). Listed under 'logic', not 'coinductive', in the bottom. "Groupoid is a multidimensional generalization of Setoid type, which has equalities on equalities and operations between them. Gropoid was introduced in algebraїс topology for the purposes of homotopy theory". Wikipedia says "Group with a partial function replacing the binary operation; Category in which every morphism is invertible. A category of this sort can be viewed as augmented with a unary operation, called inverse by analogy with group theory.", and that setoid is a special case.

todo my note: generally the syntax appears to be similar to Haskell, but the things e lists under 'logic' have things that syntactically appear to be 'constructors' but whose types actually seem to be mathematical rules that may be assumed about this type of object; the implications in these types appear to mean logical implication rather than a constructor for a function. This interpretation might break down at 'Groupoid', however, which has two arrows on the right side instead of one, and which just has 'Groupoid' at the far right. My guess is that this is some sort of deep mathy category theory meta Curry–Howard?-correspondence-style stuff in which types are literally being unified with logical statements, and that Groupoid (which, you notice, is also the only recursive and dependent and coinductive thing here, and also has itself on the right-hand side of one of the types of its constructors) is more complicated than the rest, making its signature harder to interpret. Note that the DNS domain name is 'groupoid.space', so groupoid are probably some sort of be-all end-all meta thingee in this system. Indeed, [8] says "...the "higher dimensional analogs of sets" correspond to infinity groupoids and that categories should be considered as higher-dimensional analogs of partially ordered sets.".

todo my note: why does equality only have the reflexivity property, not symmetry and transitivity? Maybe this is some weird homotopy type theory thing.

todo my note: ":=" seems to precede giving a bunch of constructors

todo my note: note that IO, AST, and PROCESS don't have explanatory text at the bottom.

todo there are other pages at the Om/EXE website that i didn't quote here b/c i don't understand them enough; there's one that gives type judgement inference rules, and one called 'Lambek encoding' that gives "Categorical Semantics of Inductive Encodings". (they say "We call such encoding in honor of Lambek lemma that leads us to the equality of (co)initial object and (co)limit in the categories of (co)algebras. ")

http://groupoid.space/exe.htm again, mostly direct quotes and paraphrases:

Syntax Tree data Exe: * := (om: Om → Exe) (core: Macro → Exe) (eff: Effect → Exe)

Language Forms

    <> ::= #option
    [] ::= #list
     I ::= #identifier
     U ::= * < #number >
     O ::= I | ( O ) | U | O → O | O O | ∀ ( I : O ) → O | λ ( I : O ) → O
     L ::= I | L I
     A ::= O | A → A | ( L : O )
     F ::= ∅ | F ( I : O ) | ()
     E ::= O | E data L : A := F
             | E record L : A < extend F > := F
             | E let F in E
             | E case E [ | I O → E ]
             | E receive E [ | I O → E ]
             | E spawn E raise L := E
             | E send E to E

Calculus

The type system is completely described by the PTS SAR notation, given by Barendregt. Find more info in Axioms and Inference Rules of underlying Om intermediate language.

   record PTS: * :=
       (S: ∀ (n: nat) → star n)
       (A: ∀ (i: nat) → type i (succ i))
       (R: ∀ (i: nat) → ∀ (j: nat) → pitype i j (max i j))

Macrosystem

Om Om language is the macrosystem terminal language. Language forms of pure Macro or inpure Effect types are expanded to the terminal language. For the details please refer to the Om Assembler description.

Om has constructors: star, var, app, arrow, pi

Om

Macro:

"Macro language subsystem is the core of Exe language and dedicated to compile the prelude described in the Core Types document. Om language is the target language of macroexpansions of data and record inductive constructions, let construction and univariable case pattern matching."

data Macro: record, data, let, case

Effects: "Effect syntax extensions defined basic process calculus axioms, IO and exception handling."

RECEIVE, TRY, RAISE, DO are listed at the top but have no details below.

todo ??: not listed above, but listed below under 'effects': "record Process: (Sigma: *) → (X: *) → * := (action: Sigma → X → GenServer? X)"

http://groupoid.space/om.htm (the following is mostly direct or paraphrased quotes from that page):

Calculus of Constructions

The Om language is a dependently typed lambda calculus, an extension of Barendregt' and Coquand Calculus of Constructions with the predicative hierarchy of indexed universes. There is no fixpoint axiom needed for the definition of infinity term dependance.

Axioms and Inference Rules

All terms respect ranking A inside sequence of universes S and complexity of the dependent term is equal maximum complexity of term and its dependency R. The type system is completely described by the following PTS notation (due to Barendregt):

    S = *{n}, n : nat
    A = *{i} : *{i+1}
    R = *{i} -> *{j} : *{max i j}

Syntax The untyped lambda language is the simplest language used in Om to generate backend programs. This subset of Om is used as the output of type erasure.

    I ::= #identifier
    T ::= I | ( T ) | T T | λ I → T

The terms of Om consist of NN-indexed stars, variables, applications, lambda-abstractions and universal quantifications (Pi-types). This language is called Calculus of Construction and exists in various syntaxes. Om supports Morte's CoC? syntax.

   <> ::= #option
    I ::= #identifier
    U ::= * < #number >
    O ::= U | I | ( O ) | O O | λ ( I : O ) → O
                      | O → O | ∀ ( I : O ) → O

AST

  data om: star (nat), var (name), app (om -> om), lambda (name -> om -> om), arrow (om -> om), pi (name -> om -> om)

TLA+

---

KIV

http://www.isse.uni-augsburg.de/en/software/kiv/

"Microsoft's Dafny -- an imperative, non-functional (I think) language -- is a very popular choice in verification challenges (alongside tools like KIV and Why3). " -- [10]

Ott

http://www.cl.cam.ac.uk/~pes20/ott/

Proof language Links