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: Contribution to journalArticle

2 Citations (Scopus)

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 arbitrary data types. 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 diverging programs.

Original languageEnglish (US)
Pages (from-to)19-46
Number of pages28
JournalProgress in Informatics
Issue number10
DOIs
StatePublished - Mar 1 2013

Fingerprint

Computer programming languages
Semantics
semantics
programming language
language
Values
programming
Acoustic waves

Keywords

  • Design
  • Languages
  • Theory
  • Verification

ASJC Scopus subject areas

  • Computer Science(all)
  • Library and Information Sciences

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.

In: Progress in Informatics, No. 10, 01.03.2013, p. 19-46.

Research output: Contribution to journalArticle

Kimmell, G, Stump, A, Eades, HD, Fu, P, Sheard, T, Weirich, S, Casinghino, C, Sjöberg, V, Collins, N & Ahn, KY 2013, 'Equational reasoning about programs with general recursion and call-by-value semantics', Progress in Informatics, no. 10, pp. 19-46. https://doi.org/10.2201/NiiPi.2013.10.3
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. In: Progress in Informatics. 2013 ; No. 10. pp. 19-46.
@article{0d205447bed246aaada8067b5600b393,
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 arbitrary data types. 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 diverging 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 = "2013",
month = "3",
day = "1",
doi = "10.2201/NiiPi.2013.10.3",
language = "English (US)",
pages = "19--46",
journal = "NII Journal",
issn = "1349-8614",
publisher = "National Institute of Informatics",
number = "10",

}

TY - JOUR

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 - 2013/3/1

Y1 - 2013/3/1

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 arbitrary data types. 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 diverging 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 arbitrary data types. 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 diverging programs.

KW - Design

KW - Languages

KW - Theory

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=84877641121&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84877641121&partnerID=8YFLogxK

U2 - 10.2201/NiiPi.2013.10.3

DO - 10.2201/NiiPi.2013.10.3

M3 - Article

AN - SCOPUS:84877641121

SP - 19

EP - 46

JO - NII Journal

JF - NII Journal

SN - 1349-8614

IS - 10

ER -