ALF ("Another logical framework") is a structure editor for monomorphic

Martin-Löf type theory Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and p ...

developed at

Chalmers University Chalmers University of Technology ( sv, Chalmers tekniska högskola, often shortened to Chalmers) is a Swedish university located in Gothenburg that conducts research and education in technology and natural sciences at a high international lev ...

. It is a predecessor of the Alfa, Agda,

Cayenne Cayenne (; ; gcr, Kayenn) is the capital city of French Guiana, an overseas region and department of France located in South America. The city stands on a former island at the mouth of the Cayenne River on the Atlantic coast. The city's m ...

and

Coq Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proo ...

proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...

s and

dependently typed programming language In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifier ...

s. It was the first language to support inductive families and dependent pattern matching.

Thorsten Altenkirch Thorsten Altenkirch ( , ) is a German Professor of Computer Science at the University of Nottingham known for his research on logic, type theory, and homotopy type theory. Altenkirch was part of the 2012/2013 special year on univalent foundatio ...

Conor McBride Conor McBride (born 18 February 1973) is a Reader in the department of Computer and Information Sciences at the University of Strathclyde. In 1999, he completed a Doctor of Philosophy (Ph.D.) in ''Dependently Typed Functional Programs and thei ...

and James McKinna (2005)
"Why Dependent Types Matter"

References

External links

Alfa
{{comp-sci-stub Academic programming languages Dependently typed languages Proof assistants

References

Further reading

External links