Abstract
In this paper we present a new natural deduction calculus for structured algebraic specifications and study proof transformations including cut elimination. As underlying language we choose an ASL-like kernel language which includes operators for composing specifications, renaming the signature and exporting a subsignature of a specification. To get a natural deduction calculus for structured specifications we combine a natural deduction calculus for first-order predicate logic with the proof rules for structured specifications. The main results are soundness and completeness of the calculus and convergence of the associated system of proof term reductions which extends a typed l-calculus by appropriate structural reductions.
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
D.R. Aspinall: Type Systems for Modular Programs and Specifications. PhD thesis, Univ. of Edinburgh, 1997.
F. Baader, T. Nipkow: Term Rewriting and All That, Cambridge Univ. Press, 1998.
H. Barendregt: The Lambda Calculus: Its Syntax and Semantics. Studies in Logics and the Foundations of Mathematics 103, Amsterdam: Elsevier, 1984.
U. Berger, H. Schwichtenberg: Program development by proof transformation. In H. Schwichtenberg (ed.): Proof and Computation, Springer ASI Series 139, 1995, 1–46.
J.A. Bergstra, J. Heering, P. Klint: Module algebra. J. ACM 37, 1990, 335–372.
M.V. Cengarle: Formal specifications with higher-order parameterization. PhD thesis, LMU München, 1995.
J.N. Crossley, J.C. Sherpherdson: Extracting programs from proofs by an extension of the Curry-Howard process. In J.N. Crossley et al. (eds.): Logical Methods, Boston: Birkhäuser, 1993.
J. Farres-Casals: Verification in ASL and related specification languages. PhD thesis, Univ. of Edinburgh, 1992.
G. Gentzen: Untersuchungen über das logische Schlieβen. Math. Zeitschrift 39, 1934, 176–210, 405-431.
J. Girard, Y. Lafont, P. Taylor: Proofs and Types. Cambridge Tracts in TCS 7, 1990.
R. Hennicker: Structured specifications with behavioural operators: Semantics, proof methods and applications. Habilitation thesis, LMU München, 1997.
R. Harper, D. Sannella, A. Tarlecki: Structure and representation in LF. In: Proc. 4th LICS `89, Asilomar, California, 1989, 226–237.
R. Hennicker, M. Wirsing: Proof systems for structured algebraic specifications: An overview. In B. Chlebus, L. Czaja (eds.): FCT `97, LNCS 1279, Springer, 1997, 19–37.
H. Peterreins: A natural-deduction-like calculus for structured specifications. PhD thesis, LMU München, 1996.
D. Sannella, R. M. Burstall: Structured theories in LCF. In G. Ausiello, M. Protasi (eds.): 8th CAAP, L’Aquila. LNCS 159, Springer, 1983, 377–391.
M. Wirsing: Algebraic specification. In J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Elsevier, Amsterdam, 1990, 675–788.
M. Wirsing: Structured specifications: syntax, semantics and proof calculus. In: F.L. Bauer et al. (eds.): Logic and Algebra of Specification, Springer, 1993, 411–442.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wirsing, M., Crossley, J.N., Peterreins, H. (1999). Proof Normalization of Structured Algebraic Specifications Is Convergent. In: Fiadeiro, J.L. (eds) Recent Trends in Algebraic Development Techniques. Lecture Notes in Computer Science, vol 1589. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48483-3_21
Download citation
DOI: https://doi.org/10.1007/3-540-48483-3_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66246-4
Online ISBN: 978-3-540-48483-7
eBook Packages: Springer Book Archive