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.
| Original language | English (US) |
|---|---|
| Title of host publication | POPL |
| Subtitle of host publication | PLPV'12 - Proceedings of the 6th Workshop on Programming Languages Meets Program Verification |
| Pages | 15-25 |
| Number of pages | 11 |
| DOIs | |
| State | Published - Mar 5 2012 |
| Event | 6th Workshop on Programming Languages Meets Program Verification, PLPV'12, Co-located with POPL 2012 - Philadelphia, PA, United States Duration: Jan 24 2012 → Jan 24 2012 |
Publication series
| Name | Conference Record of the Annual ACM Symposium on Principles of Programming Languages |
|---|---|
| ISSN (Print) | 0730-8566 |
Other
| Other | 6th Workshop on Programming Languages Meets Program Verification, PLPV'12, Co-located with POPL 2012 |
|---|---|
| Country | United States |
| City | Philadelphia, PA |
| Period | 1/24/12 → 1/24/12 |
Fingerprint
Keywords
- Design
- Languages
- Theory
- Verification
ASJC Scopus subject areas
- Software
Cite this
Equational reasoning about programs with general recursion and call-by-value semantics. / Kimmell, Garrin; Stump, Aaron; Eades, Harley D; Fu, Peng; Sheard, Tim; Weirich, Stephanie; Casinghino, Chris; Sjöberg, Vilhelm; Collins, Nathan; Ahn, Ki Yung.
POPL: PLPV'12 - Proceedings of the 6th Workshop on Programming Languages Meets Program Verification. 2012. p. 15-25 (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
}
TY - GEN
T1 - Equational reasoning about programs with general recursion and call-by-value semantics
AU - Kimmell, Garrin
AU - Stump, Aaron
AU - Eades, Harley D
AU - Fu, Peng
AU - Sheard, Tim
AU - Weirich, Stephanie
AU - Casinghino, Chris
AU - Sjöberg, Vilhelm
AU - Collins, Nathan
AU - Ahn, Ki Yung
PY - 2012/3/5
Y1 - 2012/3/5
N2 - 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.
AB - 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.
KW - Design
KW - Languages
KW - Theory
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=84857603016&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84857603016&partnerID=8YFLogxK
U2 - 10.1145/2103776.2103780
DO - 10.1145/2103776.2103780
M3 - Conference contribution
SN - 9781450311250
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 15
EP - 25
BT - POPL
ER -