KnowledgeBase » 
SEMINAR
» ID = 615
Adapting Proofs-as-Programs for the Synthesis of Imperative SML Programs
by Iman Poernomo
2003-2004
Abstract
The Curry-Howard isomorphism says that intuitionistic logic can be presented as a constructive type theory in which proofs correspond to terms, formulae to types, logical rules to type inference and proof normalization to term simplification. In order to represent intuitionistic proofs, terms of the constructive type theory contain constructive information used to prove formulae. This information can be used to synthesize correct, error-free programs from proofs. Such approaches to program synthesis, based upon the Curry-Howard isomorphism, consistute the area referred to as the proofs-as-programs paradigm. The advantage of proofs-as-programs techniques is that the task of programming a function is reduced to reasoning with domain knowledge. After more than 30 years of research, proofs-as-programs constitutes a mature field with an established theory and set of best practices. State-of-the-art approaches to proofs-as-programs usually involve some form of optimization and extraction strategy, transforming intuitionistic proofs to a commonly used functional programming language that can encode a simply typed lambda caclulus, such as SML, Scheme or Haskell.
Work has been done in providing analogous results to the Curry-Howard isomorphism and proofs-as-programs for other logical systems and programming languages. However, little work has been done in identifying a general framework that generalizes the form such analogies should take over arbitrary logical calculi and programming languages. Such a framework is useful because it can then be used to guide how to go about adapting proofs-as-programs to new contexts.
This talk considers such a framework, which we call the Curry-Howard protocol. It requires an analogous property to the Curry-Howard isomorphism to hold between a given logic and type theory. However, generalizing state-of-the-art approaches to proofs-as-programs, the protocol requires an optimization and extraction strategy from proofs represented in the logical type theory to programs in a separate programming language. While program synthesis methods have been developed that conform to our protocol, such a framework has not been explicitly identified previously.
We then use the protocol to show how proofs-as-programs can be adapted to two different contexts:
- Proofs-as-imperative-programs. The Hoare logic provides a method for the simultaneous development of imperative programs and proofs of their properties. We adapt proofs-as-programs to the Hoare logic for the purpose of extending it to developing imperative programs with side-effect-free return values and views on state.
- Structured proofs-as-programs. Structured algebraic specifications are an approach to the compositional design of software systems based on the development of data types. There are proof systems that enable us to reason about structured specifications. We develop such a system and use proofs-as-programs-style techniques for the synthesis of programs from proofs about specifications, and the eventual refinement of specifications into structured code.
These adaptations constitute an exemplary justification for the applicability of the protocol to different contexts.
Author Bio
Iman Poernomo's main research interests are computational logic for program synthesis and distributed component-based software engineering. He completed a PhD on adapting proofs-as-programs with John Crossley at the School of Computer Science, Monash University, Australia, following Bachelor of Arts (Philosophy) and Bachelor of Science Honours (Pure Maths) degrees at Monash. From 2000 to 2003 he was employed as a Senior Research Scientist and then Project Leader at the Distributed Systems Technology Centre (DSTC Pty Ltd). Currently he is employed as an independent Research Fellow at the Faculty of Information Technology at Monash University.