The Open Calculus of Constructions (Part I) : An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving

Stehr, M-O.

Artykuł - szczegóły

Tytuł artykułu

The Open Calculus of Constructions (Part I) : An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving

Autorzy

Stehr M-O.

Wybrane pełne teksty z tego czasopisma

https://fi.episciences.org/

Identyfikatory

Warianty tytułu

Języki publikacji

Abstrakty

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

equational specification rewriting logic type theory

Wydawca

IOS Press

Czasopismo

Fundamenta Informaticae

Rocznik

2005

Tom

Vol. 68, nr 1/2

Strony

131--174

Opis fizyczny

Bibliogr. 68 poz.

Twórcy

autor

Stehr M-O.

University of Illinois at Urbana-Champaign Computer Science Department Urbana, IL 61801, USA, stehr@cs.uiuc.edu

Bibliografia

[1] S. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, September 1987.
[2] B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J. C . Filliatre, E. Giménez, H. Herbelin, G. Huet, H. Laulhère, C. Muñoz, C. Murthy, C. Parent-Vigouroux, P. Loiseleur, C. Paulin, A. Säıbi, and B. Werner. The Coq Proof Assistent Reference Manual, Version 6.3.1, Coq Project. Technical report, INRIA, 1999. http://logical.inria.fr/.
[3] M. J. Beeson. Towards a computation system based on set theory. Theoretical Computer Science, 60:297–340, 1988.
[4] S. Berardi. Towards amathematical analysis of the Coquand-Huet calculus of constructions and other systems in Barendregt’s cube. Technical report, Carnegie Mellon University and Universita di Torino, 1988.
[5] F. Blanqui. Inductive types in the calculus of algebraic constructions. In M. Hofmann, editor, Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings, number 2701 in Lecture Notes in Computer Science, page Inductive types in the Calculus of Algebraic Constructions. Springer-Verlag, 2003.
[6] F. Blanqui, J.-P. Jouannaud, and M. Okada. The calculus of algebraic constructions. In P. Narendran and M. Rusinowitch, editors, Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, volume 1631 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
[7] F. Blanqui, Jean-Pierre Jouannaud, andMitsuhiro Okada. Inductive data type systems. Theoretical Computer Science, 272(1-2):41–68, 2002.
[8] C. Böhm and A. Berarducci. Automatic synthesis of typed λ-programs on term algebras. Theoretical Computer Science, 39, 1985.
[9] A. Bouhoula, J.-P. Jouannaud, and J. Meseguer. Specification and proof in membership equational logic. Theoretical Computer Science, 236:35–132, 2000.
[10] L. Cardelli. A polymorphic lambda-calculus with Type:Type. Technical report, Digital Equipment Corporation, 1986.
[11] M. Clavel, F. Durán, 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
[12] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada. Towards Maude 2.0. 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 297 – 318. Elsevier, 2000.
[13] R. L. Constable, S. Allen, H. Bromely, W. Cleveland, et al. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, 1986.
[14] T. Coquand. Une theorie des constructions. PhD thesis, Université de Paris, 1985.
[15] T. Coquand. An analysis of Girard’s paradox. In First Annual Symposium on Logic in Computer Science, Cambridge, Massachusetts, 16–18 June 1986, Proceedings. IEEE, 1986.
[16] T. Coquand. Metamathematical investigations of a calculus of constructions. In P. Odifreddi, editor, Logic and Computer Science, number 31 in APIC Studies in Data Processing. Academic Press, 1990.
[17] T. Coquand and G. Huet. Constructions: A higher order proof system for mechanizing mathematics. In B. Buchberger, editor, EUROCAL’85, European Conference on Computer Algebra, Linz, Austria, April 1–3, 1985, Proceedings Volume 1: Invited Lectures, volume 203 of Lecture Notes in Computer Science. Springer-Verlag, 1985.
[18] T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76(2/3):95–120, 1988.
[19] 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.
[20] P. Dybjer. Inductive sets and families inMartin-Löf’s type theory and their set-theoretic semantics. In Logical Frameworks, pages 280–306. Cambridge University Press, 1991.
[21] P. Dybjer and A. Setzer. A finite axiomatization of inductive-recursive definitions. In J.-Y. Girard, editor, Typed Lambda Calculi and Applications. Proceedings of TLCA’99, L’Aquila, Italy, volume 1581 of Lecture Notes in Computer Science, pages 129 – 146. Springer-Verlag, 1999.
[22] J.-P. Jouannaud F. Blanqui and P.-Y. Strub. A calculus of congruent constructions. 2004.
[23] 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.
[24] J. Y. Girard. Interpretation fonctionelle et elimination des coupures dans l’arithmetique d’ordre superieur. PhD thesis, Université Paris VII, 1972.
[25] J. A. Goguen and J. Meseguer. Order-sorted algebra solves the constructor-selector, multiple-representation, and coercion problems. Information and Computation, 103:114–158, 1993.
[26] K. Grue. Map theory. Theoretical Computer Science, 102:1–133, 1992.
[27] D. J. Howe. A classical set-theoretic model of polymorphic extensional type theory. Manuscript (submitted for publication), 1997.
[28] G. Huet. Extending the calculus of construtions with Type:Type. Unpublished Manuscript, April 1987.
[29] J.-P. Jouannaud. Membership equational logic, calculus of inductive constructions, and rewrite logic. In International Workshop on Rewriting Logic and its Applications, Abbaye des Prémontrés at Pont-`a-Mousson, France, September 1998, Proceedings, volume 15 of Electronic Notes in Theoretical Computer Science. Elsevier, 1998.
[30] J.-P. Jouannaud and M. Okada. Abstract data type systems. Theoretical Computer Science, 173(2):349–391, 1997.
[31] J.-P. Jouannaud and A. Rubio. Higher-order recursive path orderings ”á la carte”. 2003.
[32] Z. Luo. A higher-order calculus and theory abstraction. Information and Computation, 90(1):107–137, 1991.
[33] Z. Luo. A unifying theory of dependent types: the schematic approach. In Proceedings of Symposium on Logical Foundations of Computer Science (Logic at Tver 92), volume 620 of Lecture Notes in Computer Science, 1992. Also as report ECS-LFCS-92-202, Department of Computer Science, Edinburgh University.
[34] Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, 1994.
[35] S. MacLane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, 1971.
[36] N. Martí-Oliet and J. Meseguer. General logics and logical frameworks. In D. Gabbay, editor, What is a Logical System?, pages 355–392. Oxford University Press, 1994.
[37] N. Martí-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. In RWLW’96, First InternationalWorkshop on Rewriting Logic and its Applications, Asilomar Conference Center, Pacific Grove, CA, USA, September 3-6, 1996, Proceedings, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, 1996. To appear in D. M. Gabbay, F. Guenthner, (eds.), Handbook of Philosophical Logic (2nd edition), Kluwer Academic Publishers.
[38] 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.
[39] P. Martin-Löf. Type Theory. Bibliopolis, 1984.
[40] J. Meseguer. Relating models of polymorphism. In Proceedings of 16th ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1989, pages 228–241. ACM Press, 1989.
[41] J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96:73–155, 1992.
[42] J. Meseguer. A logical theory of concurrent objects and its realization in the Maude language. In G. Agha, P. Wegner, and A. Yonezawa, editors, Research Directions in Concurrent Object-Oriented Programming. MIT Press, 1993.
[43] J. Meseguer. Rewriting logic as a semantic framework for concurrency. A progress report. In U. Montanari and V. Sassone, editors, CONCUR’96: Concurrency Theory, 7th International Conference, Pisa, Italy, August 26–29, 1996, volume 1119 of Lecture Notes in Computer Science, pages 331–372. Springer-Verlag, 1996.
[44] J. Meseguer. Membership algebra as a logical framework for equational specification. In F. Parisi-Presicce, editor, Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 3–7, 1997, Selected Papers, volume 1376 of Lecture Notes in Computer Science, pages 18 – 61. Springer-Verlag, 1998.
[45] J. Meseguer and N. Martí-Oliet. From abstract data types to logical frameworks. In E. Astesiano, G. Reggio, and A. Tarlecki, editors, Recent Trends in Data Type Specification, 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May 30 - June 3, 1994, Selected Papers, volume 906 of Lecture Notes in Computer Science, pages 48–80. Springer-Verlag, 1995.
[46] Y. Moschovakis. Notes on set theory. Springer-Verlag, 1994.
[47] 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.
[48] R. Nieuwenhuis, editor. Rewriting modulo in Deduction modulo, volume 2706 of Lecture Notes in Computer Science. Springer-Verlag, 2003.
[49] T. Nipkow. Higher-order critical pairs. In Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, 15–18 July 1991, Proceedings, pages 312–319. IEEE, 1991.
[50] 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.
[51] A. Pitts. Polymorphism is set-theoretic, constructively. In Category Theory and Computer Science, Proceedings, Edinburgh, 1987, volume 283 of Lecture Notes in Computer Science, pages 12–39. Springer-Varlag, 1987.
[52] R. Pollack. Implicit syntax. In G. Huet and G. Plotkin, editors, Proceedings of the First Workshop on Logical Frameworks, Antibes, May 1990, 1990. http//www.dcs.ed.ac.uk/home/lego/html/papers.html.
[53] R. Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994.
[54] J. C. Reynolds. Polymorphism is not set-theoretic. In Lecture Notes in Computer Science, volume 173, 1984.
[55] P. Rudnicki and A. Trybulec. On equivalents of well-foundedness. Jornal of Automated Reasoning, 23:197–234, 1999.
[56] J. R. Shoenfield. Axioms of set theory. In J. Barwise, editor, Handbook of Mathematical Logic, pages 321–344. North-Holland, 1977.
[57] 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.
[58] 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.un-hamburg.de/disse/810.
[59] M.-O. Stehr. Higher-order rewriting via conditional first-order rewriting in the open calculus of constructions. In Proceedings of HOR’04, 2nd InternationalWorkshop 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.ed/stehr/biblio_stehr_eng.html.
[60] 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.
[61] M.-O. Stehr, P. Naumov, and J.Meseguer. A proof-theoretic approach to HOL-Nuprl connectionwith 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.ed/stehr/biblio_stehr_eng.html.
[62] M.-O. Stehr and C. L. Talcott. PLAN in Maude: Specifying an active network programming language. In F. Gadducci and U. Montanari, editors, The 4th International Workshop on Rewriting Logic and its Applications, Pisa, Italy, September 19–21, 2002, Proceedings, volume 71 of Electronic Notes in Theoretical Computer Science. Elsevier, 2002.
[63] A. Tarski. Über Unerreichbare Kardinalzahlen. Fundamenta Mathematicae, 30:176–183, 1938.
[64] A. Tarski. On well-ordered subsets of any set. Fundamenta Mathematicae, 32:176–183, 1939.
[65] J. Terlouw. Een nadere bewijstheoretische analyse van GSTTs. Manuscript, University of Nijmegen, The Netherlands, 1989.
[66] 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.
[67] B. Werner. Sets in types, types in sets. In M. Abadi and T. Ito, editors, Theoretical Aspects of Computer Software, Third International Symposium, TACS’97, Sendai, Japan, September 23–26, 1997, Proceedings, volume 1281 of Lecture Notes in Computer Science. Springer-Verlag, 1997.
[68] A. N. Whitehead and B. Russell. Principia Mathematica (3 volumes). Cambridge University Press, 1910, 1912, 1913.

Typ dokumentu

Bibliografia

Identyfikator YADDA

bwmeta1.element.baztech-article-BUS2-0008-0037