Name
Abstract | ||
|---|---|---|
We present the type rules for a dependently typed core calculus together with a straight-forward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The article is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.3233/FI-2010-304 | Fundam. Inform. |
Keywords | Field | DocType |
tutorial implementation,example code,lambda calculus,immediate experimentation,small example program,simply-typed lambda calculus,data type,core language,dependently typed lambda calculus,straight-forward implementation,core calculus,executable interpreter,dependent types,typed lambda calculus | Deductive lambda calculus,Programming language,Typed lambda calculus,Simply typed lambda calculus,Computer science,Lambda cube,Fixed-point combinator,System F,Church encoding,Dependent type | Journal |
Volume | Issue | ISSN |
102 | 2 | 0169-2968 |
Citations | PageRank | References |
13 | 0.91 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andres Löh | 1 | 478 | 30.02 |
| Conor McBride | 2 | 752 | 47.89 |
| Wouter Swierstra | 3 | 196 | 15.46 |