• Home
  • A simple type-theoretic language: Mini-TT

A simple type-theoretic language: Mini-TT

Sourcetitle: 
From Semantics to Computer Science : Essays in Honour of Gilles Kahn
Year of publication: 
2009
PublicationType: 
Chapter in monograph, book

This paper presents a formal description of a small functional language
with dependent types. The language contains data types, mutual recursive/
inductive definitions and a universe of small types. The syntax,
semantics and type system is specified in such a way that the implementation
of a parser, interpreter and type checker is straightforward.
The main difficulty is to design the conversion algorithm in such a way
that it works for open expressions. The paper ends with a complete
implementation in Haskell (around 400 lines of code).

http://dx.doi.org/10.1017/CBO9780511770524.007

Sourcepages: 
139-164
To the top

Page updated: 2012-01-30 14:01

Send as email
Print page
Show as pdf

X
Loading