Abstract
In a series of papers we have been using a modification of the ideas of Curry and Howard to obtain reliable programs from formal proofs. In this paper we extend our earlier work by presenting a new approach for constructing correct SML structures and SML functors from CASL structured and parametrized Specifications by extracting the SML programs from constructive proofs of the axioms of the specifications. We provide a novel formal calculus with rules corresponding to the construction and instantiation of parametrized Specifications and then a program extraction procedure which produces SML programs that meet their Specifications.
Research partly supported by ARC grant A 49230989.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
U. Berger and H. Schwichtenberg, Program development by Proof Transformation, pp. 1–45 in Proceedings of the NATO Advanced Study Institute on Proof and Computation, Marktoberdorf, Germany, 1993.
M. V. Cengarle, Formal Specifications with higher-order parametrization. PhD thesis, Ludwig-Maximilians-Universität, Munich, 1995.
CoFILanguage Design Task Group on Language Design, CASL, The Common Algebraic Specification Language, Summary, 25 March 2001, available at http://www.brics.dk/Projects/CoFI/Documents/CASL/Summary/ (accessed 28.05.2001).
R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. Harper, D. J. Howe, T. B. Knoblock, N. P. Panangaden, J. T. Sasaki, and S. F. Smith, Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.
J. N. Crossley and I. Poernomo, Fred: An approach to generating real, correct, reusable programs from proofs, FMTOOLS 2000, special issue of J.U.C.S., 7, no.1, 71–88, available at http://www.jucs.org/jucs_7_1/fred_an_approach_to (accessed 28.05.2001).
J. N. Crossley, I. Poernomo and M. Wirsing, Extraction of Structured Programs from Specification Proofs, pp. 419–437 in D. Bert, C. Choppy and P. Mosses (eds), Recent Trends in Algebraic Development Techniques (WADT’99), Lecture Notes in Computer Science 1827, Berlin: Springer, 2000.
J. N. Crossley and J. C. Shepherdson, Extracting programs from proofs by an extension of the Curry-Howard process, pp. 222–288 in J. N. Crossley, J. B. Remmel, R. A. Shore, and M. E. Sweedler (eds),Logical Methods, Birkhäuser, Boston, 1993.
J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and types, Cambridge University Press, 1989.
S. Hayashi and H. Nakano, PX, a computational logic. MIT Press, Cambridge, Mass., 1988.
G. Huet, G. Kahn, and C. Paulin-Mohring. The Coq Proof assistant Reference Manual: Version 6.1. Coq project research report RT-0203, Inria, 1997.
S. Kahrs, D. Sannella and A. Tarlecki, The definition of Extended ML: A gentle introduction. Theoretical Computer Science, 173 (1997) 445–484.
Per Martin-Löf, Intuitionistic Type Theory, Bibliopolis, Naples, Italy, 1984.
R. Milner, M. Tofte, and R. Harper, The definition of Standard ML. Cambridge, Mass., MIT Press, 1990.
F. Orejas. Structuring and modularity, pp. 159–200 in E. Astesiano, H.-J. Kreowski, B. Krieg-Bruckner (eds), Algebraic Foundations of Systems Specification, IFIP State-of-the-Art Reports. Berlin, Springer, 1999.
L. C. Paulson, ML for the Working Programmer, second edition. Cambridge University Press, 1996.
H. Peterreins, A natural-deduction-like calculus for structured Specifications. PhD thesis, Ludwig-Maximilians-Universität, Munich, 1996.
D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology, pp 375–389 in J. Diaz and F. Orejas (eds), TAPSOFT’ 89, vol. 2, Lecture Notes in Computer Science 352, Berlin, Springer 1989.
D.R. Smith, Constructing Specification Morphisms, Journal of Symbolic Computation, 15 (1993) 571–606
M. Wirsing, Structured algebraic Specifications: a kernel language, Theoretical Computer Science, 43 (1986) 123–250.
M. Wirsing, Algebraic Specification, pp.675–788in J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science, volume B, Amsterdam; New York: Elsevier; Cambridge, Mass.: MIT Press, 1990.
M. Wirsing, J. N. Crossley and H. Peterreins, Proof normalization of structured algebraic Specifications is convergent, pp. 322–337 in J. Fiadeiro (ed.), Proceedings of the Twelfth International Workshop on Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science 1589, Berlin, Springer, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Poernomo, I., Crossley, J.N., Wirsing, M. (2002). Programs, Proofs and Parametrized Specifications. In: Cerioli, M., Reggio, G. (eds) Recent Trends in Algebraic Development Techniques. WADT 2001. Lecture Notes in Computer Science, vol 2267. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45645-7_14
Download citation
DOI: https://doi.org/10.1007/3-540-45645-7_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43159-6
Online ISBN: 978-3-540-45645-2
eBook Packages: Springer Book Archive