Copertina

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

Descrizione completa

Salvato in:
Autore principale: Bove, Ana (author)
Natura: masterThesis
Lingua:inglese
Pubblicazione: 1995
Soggetti:
PROGRAMACION FUNCIONAL
ALF
TEORIA DE TIPOS
TYPE THEORY
FUNCTIONAL PROGRAMMING
Accesso online:http://hdl.handle.net/20.500.12008/2912
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1868890208823410688
author Bove, Ana
author_browse Bove, Ana
author_facet Bove, Ana
author_role author
collection COLIBRI
dc.creator.none.fl_str_mv Bove, Ana
dc.date.none.fl_str_mv 1995
2014-11-24T22:35:28Z
2014-11-24T22:35:28Z
20141202
dc.format.none.fl_str_mv 49 p.
application/pdf
dc.identifier.none.fl_str_mv BOVE, A. "A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis". Tesis de maestría, Universidad de la República (Uruguay). Facultad de Ingeniería. Instituto de Computación – PEDECIBA, 1995.
http://hdl.handle.net/20.500.12008/2912
dc.language.none.fl_str_mv en
eng
dc.publisher.none.fl_str_mv UR. FI-INCO,
dc.rights.none.fl_str_mv info:eu-repo/semantics/openAccess
Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)
dc.source.none.fl_str_mv reponame:COLIBRI
instname:Universidad de la República
instacron:Universidad de la República
dc.subject.none.fl_str_mv PROGRAMACION FUNCIONAL
ALF
TEORIA DE TIPOS
TYPE THEORY
FUNCTIONAL PROGRAMMING
dc.title.none.fl_str_mv A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
dc.type.none.fl_str_mv Tesis de maestría
info:eu-repo/semantics/masterThesis
info:eu-repo/semantics/acceptedVersion
description 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.
eu_rights_str_mv openAccess
format masterThesis
id anni_dc5c26561c72a9e885baee41ea2a98cd
identifier_str_mv BOVE, A. "A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis". Tesis de maestría, Universidad de la República (Uruguay). Facultad de Ingeniería. Instituto de Computación – PEDECIBA, 1995.
instacron_str Universidad de la República
institution Universidad de la República
instname_str Universidad de la República
language eng
language_invalid_str_mv en
network_acronym_str anni
network_name_str oai-lr-anni
oai_identifier_str oai:colibri.udelar.edu.uy:20.500.12008/2912
publishDate 1995
publishDateSort 1995
publisher.none.fl_str_mv UR. FI-INCO,
reponame_str COLIBRI
repository.mail.fl_str_mv
repository.name.fl_str_mv
repository_id_str
rights_invalid_str_mv Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)
spelling A machine assisted proof of the subject reduction property for small typed functional language. Master ThesisBove, AnaPROGRAMACION FUNCIONALALFTEORIA DE TIPOSTYPE THEORYFUNCTIONAL PROGRAMMINGWe 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.UR. FI-INCO,2014-11-24T22:35:28Z2014-11-24T22:35:28Z199520141202Tesis de maestríainfo:eu-repo/semantics/masterThesisinfo:eu-repo/semantics/acceptedVersion49 p.application/pdfBOVE, A. "A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis". Tesis de maestría, Universidad de la República (Uruguay). Facultad de Ingeniería. Instituto de Computación – PEDECIBA, 1995.http://hdl.handle.net/20.500.12008/2912reponame:COLIBRIinstname:Universidad de la Repúblicainstacron:Universidad de la RepúblicaenengLas obras depositadas en el Repositorio se rigen por la Ordenanza de los Derechos de la Propiedad Intelectual de la Universidad De La República. (Res. Nº 91 de C.D.C. de 8/III/1994 – D.O. 7/IV/1994) y por la Ordenanza del Repositorio Abierto de la Universidad de la República (Res. Nº 16 de C.D.C. de 07/10/2014)info:eu-repo/semantics/openAccessLicencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)oai:colibri.udelar.edu.uy:20.500.12008/29122026-04-14T10:27:48Z
spellingShingle A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
Bove, Ana
PROGRAMACION FUNCIONAL
ALF
TEORIA DE TIPOS
TYPE THEORY
FUNCTIONAL PROGRAMMING
status_str acceptedVersion
title A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
title_full A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
title_fullStr A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
title_full_unstemmed A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
title_short A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
title_sort A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
topic PROGRAMACION FUNCIONAL
ALF
TEORIA DE TIPOS
TYPE THEORY
FUNCTIONAL PROGRAMMING
url http://hdl.handle.net/20.500.12008/2912

Documenti analoghi