Equational reasoning about programs with general recursion and call-by-value semantics

Garrin Kimmell, Aaron Stump, Harley D. Eades, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, Ki Yung Ahn

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations

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 languageEnglish (US)
Title of host publicationPOPL
Subtitle of host publicationPLPV'12 - Proceedings of the 6th Workshop on Programming Languages Meets Program Verification
Pages15-25
Number of pages11
DOIs
StatePublished - Mar 5 2012
Externally publishedYes
Event6th Workshop on Programming Languages Meets Program Verification, PLPV'12, Co-located with POPL 2012 - Philadelphia, PA, United States
Duration: Jan 24 2012Jan 24 2012

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other6th Workshop on Programming Languages Meets Program Verification, PLPV'12, Co-located with POPL 2012
CountryUnited States
CityPhiladelphia, PA
Period1/24/121/24/12

    Fingerprint

Keywords

  • Design
  • Languages
  • Theory
  • Verification

ASJC Scopus subject areas

  • Software

Cite this

Kimmell, G., Stump, A., Eades, H. D., Fu, P., Sheard, T., Weirich, S., Casinghino, C., Sjöberg, V., Collins, N., & Ahn, K. Y. (2012). Equational reasoning about programs with general recursion and call-by-value semantics. In POPL: PLPV'12 - Proceedings of the 6th Workshop on Programming Languages Meets Program Verification (pp. 15-25). (Conference Record of the Annual ACM Symposium on Principles of Programming Languages). https://doi.org/10.1145/2103776.2103780