Conference proceeding
Equational reasoning about programs with general recursion and call-by-value semantics
Proceedings of the sixth workshop on programming languages meets program verification, pp.15-26
PLPV '12
01/24/2012
DOI: 10.1145/2103776.2103780
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 others. 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 unsound 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 Sjöberg - University of PennsylvaniaNathan Collins - Portland State UniversityKi Yung Ahn - Portland State University
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the sixth workshop on programming languages meets program verification, pp.15-26
- Publisher
- ACM
- Series
- PLPV '12
- DOI
- 10.1145/2103776.2103780
- ISSN
- 0730-8566
- Language
- English
- Date published
- 01/24/2012
- Academic Unit
- Computer Science
- Record Identifier
- 9984259405702771
Metrics
1 Record Views