Name
Abstract | ||
|---|---|---|
We give a short introduction to Martin-Löf's Type Theory, seen as a theory of inductive definitions. The first part contains historical remarks that motivate this approach. The second part presents a computational semantics, which explains how proof trees can be represented using the notations of functional programming. |
Year | DOI | Venue |
|---|---|---|
1994 | 10.1007/3-540-58715-2_114 | FSTTCS |
Keywords | Field | DocType |
inductive definitions,type theory,preliminary version,functional programming,computational semantics | Discrete mathematics,Notation,Programming language,Functional programming,Computer science,Natural deduction,Computational semantics,Inductive programming,Algorithm,Type theory,Structural induction | Conference |
Volume | ISSN | ISBN |
880 | 0302-9743 | 3-540-58715-2 |
Citations | PageRank | References |
6 | 0.53 | 13 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thierry Coquand | 1 | 1537 | 225.49 |
| Peter Dybjer | 2 | 540 | 76.99 |