Loading...
Please wait, while we are loading the content...
Similar Documents
Towards Machine-checked Compiler Correctness for Higher-order Pure Functional Languages (1994)
| Content Provider | CiteSeerX |
|---|---|
| Author | Lester, David Mintchev, Sava |
| Description | . In this paper we show that the critical part of a correctness proof for implementations of higher--order functional languages is amenable to machine--assisted proof. An extended version of the lambdacalculus is considered, and the congruence between its direct and continuation semantics is proved. The proof has been constructed with the help of a generic theorem prover --- Isabelle. The major part of the problem lies in establishing the existence of predicates which describe the congruence. This has been solved using Milne's inclusive predicate strategy [5]. The most important intermediate results and the main theorem as derived by Isabelle are quoted in the paper. Keywords: Compiler Correctness, Theorem Prover, Congruence Proof, Denotational Semantics, Lambda Calculus 1 Introduction Much of the work done previously in compiler correctness concerns restricted subsets of imperative languages. Some studies involve machine--checked correctness---e.g. Cohn [1], [2]. A lot of research h... |
| File Format | |
| Language | English |
| Publisher Date | 1994-01-01 |
| Publisher Institution | CSL '94, European Association for Computer Science Logic, Springer LNCS |
| Access Restriction | Open |
| Subject Keyword | Theorem Prover Continuation Semantics Critical Part Imperative Language Order Functional Language Correctness Proof Compiler Correctness Inclusive Predicate Strategy Introduction Much Congruence Proof Compiler Correctness Concern Lambda Calculus Important Intermediate Result Towards Machine-checked Compiler Correctness Denotational Semantics Higher-order Pure Functional Language Major Part Generic Theorem Prover Isabelle Extended Version Main Theorem |
| Content Type | Text |
| Resource Type | Article |
