ALF (proof assistant)

For the programming language, see Algebraic Logic Functional programming language.

ALF ("Another logical framework") is a structure editor for monomorphic Martin-Löf type theory developed at Chalmers University. It is a predecessor of the Alfa, Agda, Cayenne and Coq proof assistants and dependently typed programming languages. It was the first language to support inductive families and dependent pattern matching.[1][2]

References

  1. Thierry Coquand (1992). "Pattern Matching with Dependent Types". In Bengt Nordström, Kent Petersson, and Gordon Plotkin (editors), Electronic Proceedings of the Third Annual BRA Workshop on Logical Frameworks (Båstad, Sweden).
  2. Thorsten Altenkirch, Conor McBride and James McKinna (2005). "Why Dependent Types Matter".

Further reading

External links

This article is issued from Wikipedia - version of the Monday, February 15, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.