Thumbnail
Access Restriction
Open

Author Howe, Douglas J.
Source CiteSeerX
Content type Text
Publisher Springer Verlag
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Well-typed Expression ♦ Nuprl Proof Development System ♦ Certain Combination ♦ Functional Programming Language ♦ Introduction Type System ♦ Extraction Mode ♦ Functional Program ♦ Familiar Style ♦ Conventional Program-verification Mode ♦ Majority Algorithm ♦ Mathematical Proof ♦ Language Construct ♦ Constructive Type Theory ♦ Typed Language
Description . There are two ways of reasoning about functional programs in the constructive type theory of the Nuprl proof development system. Nuprl can be used in a conventional program-verification mode, in which functional programs are written in a familiar style and then proven to be correct. It can also be used in an extraction mode, where programs are not written explicitly, but instead are extracted from mathematical proofs. Nuprl is the only constructive type theory to support both of these approaches. These approaches are illustrated by applying Nuprl to Boyer and Moore's "majority" algorithm. 1 Introduction A type system for a functional programming language can be syntactic or semantic. In a syntactically typed language, such as SML 1 [25], typing is a property of the syntax of expressions. Only certain combinations of language constructs are designated "well-typed", and only well-typed expressions are given a meaning. Each well-typed expression has a type which can be derive...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 1993-01-01
Publisher Institution In Functional Programming, Concurrency, Simulation and Automated Reasoning