Name
Title | ||
|---|---|---|
Correct-by-construction model transformations from partially ordered specifications in Coq |
Abstract | ||
|---|---|---|
This paper sketches an approach to the synthesis of provably correct model transformations within the Coq theorem prover, an implementation of Coquand and Huet's Calculus of Inductive Constructions. It extends work done by Poernomo on proofs-as-model-transformations in the related formalism of Martin-Löf predicative Constructive Type Theory. We show how the impredicative theory of Coq, together with its treatment of coinductive types, lends itself to the synthesis of a wider range of model transformations than Poernomo had treated before. We illustrate the practical benefits and potential scalability of our approach by means of a case study taken from industry. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-16901-4_6 | ICFEM |
Keywords | Field | DocType |
correct-by-construction model transformation,impredicative theory,coinductive type,practical benefit,coq theorem prover,model transformation,potential scalability,provably correct model transformation,inductive constructions,related formalism,case study,type theory,partial order,theorem prover | Lambda calculus,Intuitionistic type theory,Computer science,Automated theorem proving,Algorithm,Theoretical computer science,Calculus of constructions,Coinduction,Impredicativity,Formalism (philosophy),Predicative expression,Calculus | Conference |
Volume | ISSN | ISBN |
6447 | 0302-9743 | 3-642-16900-7 |
Citations | PageRank | References |
16 | 0.57 | 5 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Iman Poernomo | 1 | 428 | 27.61 |
| Jeffrey Terrell | 2 | 17 | 0.93 |