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

Towards a practical programming language based on dependent type theory

Ulf Norell (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
Göteborg : Chalmers University of Technology, 2007. ISBN: 978-91-7291-996-9.- 166 s.

Dependent type theories have a long history of being used for theorem proving. One aspect of type theory which makes it very powerful as a proof language is that it mixes deduction with computation. This also makes type theory a good candidate for programming---the strength of the type system allows properties of programs to be stated and established, and the computational properties provide semantics for the programs. This thesis is concerned with bridging the gap between the theoretical presentations of type theory and the requirements on a practical programming language. Although there are many challenging research problems left to solve before we have an industrial scale programming language based on type theory, this thesis takes us a good step along the way.

Nyckelord: type theory, programming, dependent types, pattern matching, metavariables, type checking

Denna post skapades 2007-08-31. Senast ändrad 2013-09-25.
CPL Pubid: 46311


Läs direkt!

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