Loading...
Please wait, while we are loading the content...
Similar Documents
Program Extraction in simply-typed Higher Order Logic (2002)
| Content Provider | CiteSeerX |
|---|---|
| Author | Berghofer, Stefan |
| Description | Types for Proofs and Programs (TYPES 2002), LNCS 2646 |
| Abstract | Based on a representation of primitive proof objects as #- terms, which has been built into the theorem prover Isabelle recently, we propose a generic framework for program extraction. We show how this framework can be used to extract functional programs from proofs conducted in a constructive fragment of the object logic Isabelle/HOL. A characteristic feature of our implementation of program extraction is that it produces both a program and a correctness proof. Since the extracted program is available as a function within the logic, its correctness proof can be checked automatically inside Isabelle. |
| File Format | |
| Publisher Date | 2002-01-01 |
| Publisher Institution | Technische Universität München |
| Access Restriction | Open |
| Subject Keyword | Extracted Program Program Extraction Functional Program Generic Framework Constructive Fragment Correctness Proof Primitive Proof Object Simply-typed Higher Order Logic Characteristic Feature Theorem Prover Isabelle Inside Isabelle Object Logic Isabelle Hol |
| Content Type | Text |
