Skip to main content
Article
Combining Proofs and Programs in a Dependently Typed Language
Technical Reports (CIS)
  • Stephanie Weirich, University of Pennsylvania
  • Vilhelm Sjoberg, University of Pennsylvania
  • Chris Casinghino
Document Type
Technical Report
Date of this Version
1-1-2013
Comments

University of Pennsylvania Department of Computer and Information Science Technical Report No. MS-CIS-13-08.

Postprint version. Copyright held by owner author. This is the author's version of the work.

Abstract
Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, mega). Here, we combine these two approaches into a single dependently-typed core language. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness, and a call-by-value programming language that guarantees type safety but not termination. The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can require logical proofs as arguments; and “mobile” program values, including proofs computed at runtime, may be used as evidence by the logic. This language allows programmers to work with total and partial functions uniformly, providing a smooth path from functional programming to dependently-typed programming. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory Keywords Dependent types; Termination; General recursion
Keywords
  • Dependent types,
  • Termination,
  • General recursion
Citation Information
Stephanie Weirich, Vilhelm Sjoberg and Chris Casinghino. "Combining Proofs and Programs in a Dependently Typed Language" (2013)
Available at: http://works.bepress.com/stephanie_weirich/26/