notes-computer-programming-programmingLanguagesBook-programmingLanguagesChProofLangs

Table of Contents for Programming Languages: a survey

Chapter : Proof assistant languages

Coq

Not Turing-complete (termination condition)

Agda

Not Turing-complete (termination condition) (sorta)

HOL

Succeeded by Isabelle.

Isabelle

ACL2

Not Turing-complete (termination condition)

Epigram

Not Turing-complete (termination condition)

Charity

Not Turing-complete (termination condition)