@inproceedings{95d93b1e34fc478e914bb4307214772f,
title = "Equational reasoning about programs with general recursion and call-by-value semantics",
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.",
keywords = "Design, Languages, Theory, Verification",
author = "Garrin Kimmell and Aaron Stump and Eades, {Harley D.} and Peng Fu and Tim Sheard and Stephanie Weirich and Chris Casinghino and Vilhelm Sj{\"o}berg and Nathan Collins and Ahn, {Ki Yung}",
year = "2012",
month = mar
day = "5",
doi = "10.1145/2103776.2103780",
language = "English (US)",
isbn = "9781450311250",
series = "Conference Record of the Annual ACM Symposium on Principles of Programming Languages",
pages = "15--25",
booktitle = "POPL",
note = "6th Workshop on Programming Languages Meets Program Verification, PLPV'12, Co-located with POPL 2012 ; Conference date: 24-01-2012 Through 24-01-2012",
}