A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis

Autor:	Bove, Ana
Jazyk:	angličtina
Rok vydání:	1995
Předmět:	TYPE THEORY PROGRAMACION FUNCIONAL ALF TEORIA DE TIPOS FUNCTIONAL PROGRAMMING
Zdroj:	COLIBRI Universidad de la República instacron:Universidad de la República
Popis:	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 types, and objects of these types can be view as funtional programming environments of proof assistants. The language we analyze is a small typed functional language. We present its syntax, its dynamic semanctics and its type system. Among other properties, we present a formalization pf the Subject Reduction property for the language. The proof assistant we use is ALF.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=od______3056::dc5c26561c72a9e885baee41ea2a98cd Zobrazit plný text záznamu