Table of Contents for Programming Languages: a survey

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:

- http://coq-blog.clarus.me/a-blog-engine-written-and-proven-in-coq.html
- http://matej-kosik.github.io/www/doc/coq/coq-trunk-proof-tree/index.html
- https://www.stephanboyer.com/post/134/my-unusual-hobby

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]

Succeeded by Isabelle.

1996.

Not Turing-complete (termination condition)

Not Turing-complete (termination condition)

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

'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)'

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.

MIT license.

1989

1996

"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]

"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:

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:

- No Fixpoint and Induction in Core
- Macros, eg "The language of polynomial functors (data and record) and core language of the process calculus (spawn, receive and send) is just macrosystem over CoC? language"
- "Changable Encodings. In pure CoC? we have only arrows, so all inductive type encodings would be Church-encoding variations. Most extended nowadays is Church-Boehm-Berrarducci the encoding which dedicated to inductive types. Another well known are Scott (laziness), Parigot (laziness and constant-time iterators) and CPS (continuations) encodings."
- "Proved Categorical Semantic"

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

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

- EXE - Macro Expansion
- TYPE - Typechecking
- NORMAL - Normalization
- ERASE - Type Information Erasure
- COMPACT - Compress Terms
- EXTRACT - Extract VM Lambda

Logic

- REC - Recursor
- INDUCTION - Dependent Eliminator
- EQU - Propositional Equality
- SIMPLE - Simplification, K combinator
- FREGE - Frege, S combinator
- PROP - Propositions

Macros

- CASE - Patterm Matching
- LET - Extract VM Lambda
- DATA - Inductive Definition
- RECORD - Coinductive Definition

Base Library

- IO - Input/Output Free Monad
- IOI - Infinity Input/Output Cofree Comonad
- Lazy - Lazy Type
- Bool - Boolean
- Maybe - Maybe
- Nat - Natural Number Object
- List - Inductive List
- Unit - 0-Tuple
- Mon - 1-Tuple
- Prod - 2-Tuple
- Morte - Recursive and Corecursive samples

"

[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

- : Coinductive ...

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:))

- sum: left, right (" sum is a meta-representation form of data inductive Exe syntax construction. For the internal form see Data AST construction. ") ((my note: is this sum types? (todo)))
- empty: "empty is a bottom type used as zero or terminal for sum inductive type. This type nas no constructors or with empty body. "

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

- OB: elem, eq, point
- HOM ('homomorphism'): elem, eq, point; 'elem' seems to be a mapping from one structure to another, 'eq' seems to be governed by a requirement that if x1 == x2 then elem(x1) == elem(x2), where '==' is the version of EQ in each structure, and 'point' seems to be governed by a requirement that elem(X.point) == Y.point, where X and Y are the structures standing in the homomorphic relationship (todo)

NR ND +

- BOOL: true, false; also only two functions, AND and OR
- TRUE: intro (i think 'intro' just means that in logic, you can always introduce 'true' because 'true' is always true); listed under 'logic', not 'inductive', in the bottom (todo)
- FALSE: (no constructors) (i think that just means that, in contrast to 'true', in logic you can never introduce 'false' because 'false' is never true); listed under 'logic', not 'inductive', in the bottom (todo)
- OPTION
- UNIT star; note that in the bottom, 'unit' is listed under 'coinductive', not 'inductive', but e also says "we only show how record and data are equal in example of unit and prod which are primitive forms of coinductive constructions. " (todo)

R ND +

- NAT: zero, succ
- LIST: nil, cons
- IO
- AST

NR D +

- EQ: refl (followed by the definition of reflexivity; i think that just means that in logic, reflexivity is a property of equality); listed under 'logic', not 'inductive', in the bottom (todo)
- EXISTS: intro (followed by the rule that if 'P(x) = true' and 'x : A' then 'exists A such that P'; so this is just an introduction rule for the existential quantifier); listed under 'logic', not 'inductive', in the bottom (todo)

R D +

- VECTOR: nil, cons; limited length list (depends on length, whic is NAT)

NR ND *

- PROD: either 'cons' or 'pr1' and 'pr2'; probably short for 'product'
- PURE: return
- FUNCTOR: fmap
- APPLICATIVE: ap; also says 'extend' and then something about 'pure' and 'functor'
- MONAD: join; also says 'extend' and then something about 'pure' and 'functor'

R ND *

- STREAM: head, tail; "stream is a record form of the list's cons constructor. It models the infinity list that has no terminal element. "
- PROCESS

NR D *

- SIGMA: pr1, pr2
- SETOID: ob, hom; 'hom' appear to have the attached requirement that for any X,Y in Ob, HOM(X,Y). Note that HOM is defined above as Homomorphism. Listed under 'logic', not 'coinductive', in the bottom. "Setoid in essence is a type with an equality." Wikipedia says, "In mathematics, a setoid (also called an E-set) is a set (or type) equipped with an equivalence relation...setoids may be used when a difference between identity and equivalence must be maintained"

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

- LAMBDA
- PI: listed below as "Arrow / Pi" "record Arrow Pi", with constructors name (string), arg (Om), body (Om). Note: at [9] it speaks of "universal quantifications (Pi-types)".
- APP: fun (Om), arg (Om)
- VAR: name (string)
- STAR: index (natural number) (todo: could this be like the * that means 'kind' in haskell?)

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

- DATA: (see RECORD, below)
- RECORD: listed as "Record / Data" "record Record Data" with constructors: name (string), base (Om), body (list (prod string Exe))
- LET: binds (list (prod string Exe)), in (Exe)
- CASE: listed as "Case / Receive" "record Case Receive" with constructors: of (Exe), legs (list (prod atom (prod Om Exe))), default (Exe)

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

- SPAWN: proc (Process), raise (list Eff)
- SEND: message (Sigma), to (Process Sigma)
- RECEIVE
- TRY
- RAISE
- DO

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)

---

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]

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

- survey article on proof assistants: https://www.dropbox.com/s/4mwtxojg7yqb365/Geuvers2009.pdf