Journal article
Equational reasoning about programs with general recursion and call-by-value semantics
Progress in informatics, Vol.10, pp.19-46
03/2013
DOI: 10.2201/NiiPi.2013.10.3
Abstract
Dependently typed programming languages provide a mechanism for integrating verification and programming by encoding invariants as types. Traditionally, dependently typed languages have been based on constructive type theories, where the connection between proofs and programs is based on the Curry-Howard correspondence. This connection comes at a price, however, as it is necessary for the languages to be normalizing to preserve logical soundness. Trellys is a call-by-value dependently typed programming language currently in development that is designed to integrate a type theory with unsound programming features, such as general recursion, Type:Type, and arbitrary data types. In this paper we outline one core language design for Trellys, and demonstrate the use of the key language constructs to facilitate sound reasoning about potentially diverging programs.
Details
- Title: Subtitle
- Equational reasoning about programs with general recursion and call-by-value semantics
- Creators
- Garrin Kimmell - University of IowaAaron Stump - University of IowaHarley D. EadesPeng FU - University of IowaTim Sheard - Portland State UniversityStephanie Weirich - University of PennsylvaniaChris Casinghino - University of PennsylvaniaVilhelm Sjoberg - University of PennsylvaniaNathan Collins - Portland State UniversityKi YUNG AHN
- Resource Type
- Journal article
- Publication Details
- Progress in informatics, Vol.10, pp.19-46
- DOI
- 10.2201/NiiPi.2013.10.3
- ISSN
- 1349-8614
- eISSN
- 1349-8606
- Language
- English
- Date published
- 03/2013
- Academic Unit
- Computer Science
- Record Identifier
- 9984259437902771
Metrics
16 Record Views