The Open Calculus of Constructions. Part 2, An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving

• Autorzy: Stehr M.-O.
• Języki publikacji: EN

Abstrakty

EN

The open calculus of constructions integrates key features of Martin-Löf's type theory, the calculus of constructions, membership equational logic, and rewriting logic into a single uniform language. The two key ingredients are dependent function types and conditional rewriting modulo equational theories. We explore the open calculus of constructions as a uniform framework for programming, specification and interactive verification in an equational higher-order style. By having equational logic and rewriting logic as executable sublogics we preserve the advantages of a first-order semantic and logical framework and we provide a foundation for a broad spectrum of applications ranging from what could be called executable mathematics, involving symbolic computations and logical proofs, to software and system engineering applications, involving symbolic execution and analysis of nondeterministic and concurrent systems.

Słowa kluczowe

EN

equational specification; rewriting logic; type theory

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 68, nr 3
• Strony: 249--288
• Opis fizyczny: Bibliogr. 54 poz.

Twórcy

autor

Stehr M.-O.

• University of Illinois at Urbana-Champaign Computer Science Department Urbana, IL 61801, USA,

Bibliografia

• [1] S. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, September 1987.
• [2] L. Augustsson. Cayenne - a language with dependent types. In S. D. Swierstra, P. R. Henriques, and J. N. Oliveira, editors, Advanced Functional Programming, Third International School, Braga, Portugal, September 12-19, 1998, Revised Lectures, volume 1608 of Lecture Notes in Computer Science, pages 240-267. Springer-Verlag, 1999.
• [3] M. J. Beeson. Towards a computation system based on set theory. Theoretical Computer Science, 60:297-340, 1988.
• [4] E. Bonelli, D. Kesner, and A. Ríos. A de Bruijn notation for higher-order rewriting. In Proceedings of the 11th International Conference on Rewriting Techniques and Applications (RTA’00), Norwick, UK, July 2000, volume 2051 of Lecture Notes in Computer Science, pages 62-79. Springer-Verlag, 2001.
• [5] E. Bonelli, D. Kesner, and A. Ríos. From higher-order to first-order rewriting. In Proceedings of the 12th International Conference on Rewriting Techniques and Applications (RTA’01), Utrecht, The Netherlands, June 2001, volume 2051 of Lecture Notes in Computer Science, pages 47-62. Springer-Verlag, 2001.
• [6] A. Bouhoula, J.-P. Jouannaud, and J. Meseguer. Specification and proof in membership equational logic. Theoretical Computer Science, 236:35-132, 2000.
• [7] I. Cervesato, N. Durgin, P. D. Lincoln, J. C. Mitchell, and A. Scedrov. Relating Strands and Multiset Rewriting for Security Protocol Analysis. In 13th Computer Security Foundations Workshop, pages 35-51. IEEE Computer Society Press, 2000.
• [8] I. Cervesato and M.-O. Stehr. Representating the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types. In Fifth International Workshop on Rewriting Logic and its Applications (WRLA’2004), Barcelona, Spain, March 27 - 28, 2004, Electronic Notes in Theoretical Computer Science. Elsevier, 2004. http://formal.cs.uiuc.edu/stehr/msr.html.
• [9] K. Chen, P. Hudak, andM. Odersky. Parametric type classes. In Proceedings of the ACM conference on LISP and Functional Programming, San Francisco, California, June 22-24, 1992. ACM Press, 1992.
• [10] M. Clavel, F. Dur´an, S. Eker, P. Lincoln, N. Mart´ı-Oliet, J. Meseguer, and J. Quesada. Maude: Specification and Programming in Rewriting Logic. SRI International, January 1999. http://maude.csl.sri.com.
• [11] A. Coja-Oghlan and M.-O. Stehr. Revisiting the algebra of Petri net processes under the collective token philosophy. Fundamenta Informaticae, 54:151 - 164, 2003.
• [12] R. L. Constable, S. Allen, H. Bromely, W. Cleveland, et al. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, 1986.
• [13] T. Coquand. Infinite objects in type theory. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs: International Workshop TYPES’93, Nijmegen, May 1993, Selected Papers, volume 806 of Lecture Notes in Computer Science, pages 19-61. Springer-Verlag, 1993.
• [14] T. Coquand and C. Paulin-Mohring. Inductively defined types. In COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, volume 417 of Lecture Notes in Computer Science. Springer-Verlag, 1990.
• [15] S. Feferman. A language and axioms for explicit mathematics. In J. N. Crossley, editor, Algebra and Logic, volume 450 of Lecture Notes in Mathematics, pages 87-139. Springer-Verlag, 1975.
• [16] E. Giménez. Codifying guarded definitions with recursive schemes. In BRA Workshop on Types for Proofs and Programs (TYPES’94), volume 996 of Lecture Notes in Computer Science, pages 39-59, 1994.
• [17] J. Goguen and G. Malcolm. A hidden agenda. Theoretical Computer Science, 245(1):55-101, August 2000. Special Issue on Algebraic Engineering edited by C. Nehaniv and M. Ito.
• [18] K. Grue. Map theory. Theoretical Computer Science, 102:1-133, 1992.
• [19] D. J. Howe. Importing mathematics from HOL into Nuprl. In J. Von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs’96, Turku, Finland, August 26-30, 1996, Proceedings, volume 1125 of Lecture Notes in Computer Science, pages 267-282. Springer Verlag, 1996.
• [20] D. J. Howe. Semantical foundations for embedding HOL in Nuprl. In M. Wirsing and M. Nivat, editors, AlgebraicMethodology and Software Technology, volume 1101 of Lecture Notes in Computer Science, pages 85-101, Berlin, 1996. Springer-Verlag.
• [21] D. J. Howe. A classical set-theoretic model of polymorphic extensional type theory. Manuscript (submitted for publication), 1997.
• [22] D. J. Howe. A type annotation scheme for Nuprl. In J. Grundy and M. C. Newey, editors, Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs’97, Canberra, Australia, September 27-October 1, 1998, Proceedings, volume 1479 of Lecture Notes in Computer Science, pages 207-224. Springer-Verlag, 1998.
• [23] D. J. Howe and S. Stoller. An operational approach to combining classical set theory and functional programming languages. In M. Hagiya and J. C. Mitchell, editors, Theoretical Aspects of Computer Software, Third International Symposium, TACS’94, Sendai, Japan, April 19-22, 1994, Proceedings, volume 789 of Lecture Notes in Computer Science, pages 36-55. Springer-Verlag, 1994.
• [24] G. Huet and A. Saïbi. Constructive category theory. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 1998.
• [25] B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222-259, 1997.
• [26] M. P. Jones. Qualified Types: Theory and Practice. PhD thesis, Programming Research Group, Oxford University Computing Laboratory, July 1992. Published by Cambridge University Press, November 1994.
• [27] M. P. Jones. A theory of qualified types. In B. Krieg-Brückner, editor, ESOP’92: 4th European Symposium on Programming, Rennes, France, February 26-28, 1992, Proceedings, volume 582 of Lecture Notes in Computer Science. Springer-Verlag, 1992.
• [28] M. P. Jones. Type classes with functional dependencies. In Proceedings of the 9th European Symposium on Programming, ESOP 2000, Berlin, Germany, March 2000, volume 1782 of Lecture Notes in Computer Science. Springer-Verlag, 2000.
• [29] S. Peyton Jones, M. Jones, and E. Meijer. Type classes: Exploring the design space. In Proceedings of the Second Haskell Workshop, Amsterdam, June 1997, 1997.
• [30] B. Lampson and R. Burstall. Pebble, a kernel language for modules and abstract data types. Information and Computation, 76(2/3):278-346, 1988.
• [31] Z. Luo. A higher-order calculus and theory abstraction. Information and Computation, 90(1):107-137, 1991.
• [32] Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, 1994.
• [33] D. MacQueen. Using dependent types to express modular structure. In Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, pages 277-286, 1986.
• [34] P. Martin-Löf. An intuitionistic theory of types: Predicative part. In H. Rose and J. Shepherdson, editors, Logic Colloquium 73, pages 73-108. North-Holland, 1974.
• [35] J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96:73-155, 1992.
• [36] J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, January 1985, pages 37-51, 1985.
• [37] P. Naumov, M.-O. Stehr, and J. Meseguer. The HOL/NuPRL proof translator — A practical approach to formal interoperability. In Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs’2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, volume 2152 of Lecture Notes in Computer Science, pages 329-345. Springer-Verlag, 2001.
• [38] C. Paulin-Mohring. Inductive Definitions in the system Coq - Rules and Properties. In M. Bezem and J . F. Groote, editors, Typed Lambda Calculi and Applications, International Conference, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science. Springer Varlag, 1993.
• [39] K. Petersson, J. Smith, and B. Nordstroem. Programming in Martin-Löf ’s Type Theory. An Introduction. International Series of Monographs on Computer Science. Oxford: Clarendon Press, 1990.
• [40] F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN’88 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, 22-24 June 1988, SIGPLAN Notices 23(7), pages 199-208, 1988.
• [41] R. Pollack. Closure under alpha-conversion. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs: International Workshop TYPES’93, Nijmegen, May 1993, Selected Papers, volume 806 of Lecture Notes in Computer Science, pages 313-332. Springer-Verlag, 1993.
• [42] R. Pollack. Programming with dependent types: Examples. Dagstuhl Seminar 01341: Dependent Type Theory meets Practical Programming, September 2001.
• [43] H. Reichel. An approach to object semantics based on terminal co-algebras. Mathematical Structures in Computer Science, pages 129-152, 1995.
• [44] D. E. Rydeheard and R. M. Burstall. Computational Category Theory. Prentice Hall, 1988.
• [45] M. Stefanova and H. Geuvers. A simple model construction for the calculus of constructions. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
• [46] M.-O. Stehr. CINNI - A Generic Calculus of Explicit Substitutions and its Application to λ-, σ-, and π-calculi. In K. Futatsugi, editor, The 3rd International Workshop on Rewriting Logic and its Applications, Kanazawa City Cultural Hall, Kanzawa, Japan, September 18-20, 2000, Proceedings, volume 36 of Electronic Notes in Theoretical Computer Science, pages 71 - 92. Elsevier, 2000.
• [47] M.-O. Stehr. Programming, Specification, and Interactive Theorem Proving-Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory. Doctoral Thesis, Universität Hamburg, Fachbereich Informatik, Germany, 2002. http://www.sub.uni-hamburg.de/disse/810/.
• [48] M.-O. Stehr. Higher-order rewriting via conditional first-order rewriting in the open calculus of constructions. In Proceedings of HOR’04, 2nd International Workshop on Higher-Order Rewriting, Aachen, Germany, June 2, 2004, number AIB-2004-03 in Aachener Informatik Berichte. Department of Computer Science, June 2004 http://formal.cs.uiuc.edu/stehr/biblio_stehr_eng.html.
• [49] M.-O. Stehr and J. Meseguer. Pure type systems in rewriting logic: Specifying typed higher-order languages in a first-order logical framework. In Essays in Memory of Ole-Johan Dahl, volume 2635 of LNCS, pages 334-375. Springer-Verlag, 2004.
• [50] M.-O. Stehr, J. Meseguer, and P. C. Őlveczky. Rewriting logic as a unifying framework for Petri nets. In H. Ehrig, G. Juhas, J. Padberg, and G. Rozenberg, editors, Unifying Petri Nets, Advances in Petri Nets, volume 2128 of Lecture Notes in Computer Science, pages 250-303. Springer-Verlag, 2001.
• [51] M.-O. Stehr, P. Naumov, and J.Meseguer. A proof-theoretic approach to HOL-Nuprl connection with applications to proof translation (extended abstract). In WADT/CoFI’01, 15th International Workshop on Algebraic Development Techniques and General Workshop of the CoFI WG, Genova, Italy, April 1 - 3, 2001, Proceedings, 2001. Full version available at http://formal.cs.uiuc.edu/stehr/biblio_stehr_eng.html.
• [52] Y. Tsukada. Martin-Löf’s type theory as an open-ended framework. International Journal of Foundations of Computer Science, 12(1):31-67, 2001.
• [53] V. van Oostrom and F. van Raamsdonk. Comparing combinatory reduction systems and higher-order rewrite systems. In HOA-93, volume 816 of Lecture Notes in Computer Science, pages 276-304. Springer-Varlag, 1993.
• [54] P. Wadler and S. Blott. How to make ad hoc polymorphism less ad hoc. In Proceedings of 16th ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1989, pages 60-76. ACM Press, 1989.