Name
Abstract | ||
|---|---|---|
An algebraic presentation of Martin-Löf's intuitionistic type theory is given which is based on the notion of a category with families with extra structure. We then present a type-checking algorithm for the normal forms of this theory, and sketch how it gives rise to an initial category with families with extra structure. In this way we obtain a purely algebraic formulation of the correctness of the type-checking algorithm which provides the core of proof assistants for intuitionistic type theory. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-78969-7_2 | FLOPS |
Keywords | Field | DocType |
extra structure,algebraic foundation,initial category,intuitionistic type theory,algebraic presentation,type-checking algorithm,normal form,proof assistant,algebraic formulation,type theory | Algebraic number,Intuitionistic type theory,Algebra,Computer science,Structural proof theory,Correctness,Proof theory,Type theory,Theoretical computer science,Sketch | Conference |
Volume | ISSN | ISBN |
4989 | 0302-9743 | 3-540-78968-5 |
Citations | PageRank | References |
4 | 0.52 | 8 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Abel | 1 | 49 | 4.61 |
| Thierry Coquand | 2 | 1537 | 225.49 |
| Peter Dybjer | 3 | 540 | 76.99 |