CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A simple type-theoretic language: Mini-TT

Thierry Coquand ; Y. Kinoshita ; Bengt Nordström (Institutionen för data- och informationsteknik (Chalmers)) ; M. Takeyama
From Semantics to Computer Science : Essays in Honour of Gilles Kahn p. 139-164. (2009)
[Kapitel]

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).

Nyckelord: type theory, programming language, dependent types, data types, recursive, type checker



Denna post skapades 2009-03-18. Senast ändrad 2011-08-18.
CPL Pubid: 91611

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU) (GU)
Institutionen för data- och informationsteknik (Chalmers)

Ämnesområden

Datavetenskap (datalogi)

Chalmers infrastruktur