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

doi:10.1145/2103776.2103780

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 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	https://doi.org/10.1145/2103776.2103780
State	Published - 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

Keywords

Design
Languages
Theory
Verification

ASJC Scopus subject areas

Software

Access to Document

10.1145/2103776.2103780

Fingerprint Dive into the research topics of 'Equational reasoning about programs with general recursion and call-by-value semantics'. Together they form a unique fingerprint.

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

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

Kimmell, G, Stump, A, Eades, HD, Fu, P, Sheard, T, Weirich, S, Casinghino, C, Sjöberg, V, Collins, N & Ahn, KY 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. Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pp. 15-25, 6th Workshop on Programming Languages Meets Program Verification, PLPV'12, Co-located with POPL 2012, Philadelphia, PA, United States, 1/24/12. https://doi.org/10.1145/2103776.2103780

Kimmell G, Stump A, Eades HD, Fu P, Sheard T, Weirich S et al. 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. 2012. p. 15-25. (Conference Record of the Annual ACM Symposium on Principles of Programming Languages). https://doi.org/10.1145/2103776.2103780

Kimmell, Garrin ; Stump, Aaron ; Eades, Harley D. ; Fu, Peng ; Sheard, Tim ; Weirich, Stephanie ; Casinghino, Chris ; Sjöberg, Vilhelm ; Collins, Nathan ; Ahn, Ki Yung. / Equational reasoning about programs with general recursion and call-by-value semantics. POPL: PLPV'12 - Proceedings of the 6th Workshop on Programming Languages Meets Program Verification. 2012. pp. 15-25 (Conference Record of the Annual ACM Symposium on Principles of Programming Languages).

@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}",

note = "Copyright: Copyright 2012 Elsevier B.V., All rights reserved.; 6th Workshop on Programming Languages Meets Program Verification, PLPV'12, Co-located with POPL 2012 ; Conference date: 24-01-2012 Through 24-01-2012",

year = "2012",

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",

}

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

Y1 - 2012

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

AN - SCOPUS:84857603016

SN - 9781450311250

T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages

SP - 15

EP - 25

BT - POPL

T2 - 6th Workshop on Programming Languages Meets Program Verification, PLPV'12, Co-located with POPL 2012

Y2 - 24 January 2012 through 24 January 2012

ER -