A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
We present an experiment in formally describing a programming language and its properties in constructive type theory. By constructive type theory we understand primarily the formulation of Martin Löf's set theory. Constructive type theory can also be seen as a programming language where we write ty...
Saved in:
| Main Author: | |
|---|---|
| Format: | masterThesis |
| Language: | English |
| Published: |
1995
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/20.500.12008/2912 |
| Tags: |
No Tags, Be the first to tag this record!
|
Similar Items: A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
- Course-of-values recursion in Martin-Löf's type theory
- Typed windows : an implementation of a programming language for graphics design. Master Thesis
- Functions in C5
- C5 printf and C5 scanfin C5 version 0.98
- A generic version of scanf programmed in C5
- Architecture and ornament: subjectivity oriented to objects and post-work politics