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

Inductive definitions and type theory an introduction (preliminary version)

Peter Dybjer (Institutionen för datavetenskap, Programmeringslogik) ; Thierry Coquand (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
Foundation of Software Technology and Theoretical Computer Science: 14th Conference Madras, India; (Lecture Notes in Computer Science; 880) Vol. 880 (1994), p. 60-76.
[Konferensbidrag, refereegranskat]

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.



Denna post skapades 2007-01-18. Senast ändrad 2015-02-12.
CPL Pubid: 17645

 

Institutioner (Chalmers)

Institutionen för datavetenskap, Programmeringslogik (2002-2004)
Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)

Ämnesområden

Annan matematik

Chalmers infrastruktur