Combining proofs and programs in a dependently typed langauge

Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or al-low 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 over-lapping 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 ex-pressions 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, includ-ing 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 func-tional programming to dependently-typed programming