Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs

• Autorzy: Abel A. , Coquand T.
• Języki publikacji: EN

Abstrakty

EN

Martin-Löf's Logical Framework is extended by strong S-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules is proven via a generic PER model on untyped terms. An algorithmic version of the framework is given through an untyped bh-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with h-equality on b-normal forms, which is shown equivalent to the algorithmic equality.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 4
• Strony: 345--395
• Opis fizyczny: bibliogr. 28 poz.

Twórcy

autor

Abel A.

autor

Coquand T.

• Institut für Informatik, Ludwigs-Maximilians-Universität München, Germany,

Bibliografia

• [1] Abel, A.: An Implementation of the Logical Framework with _-Types, Haskell code, available at http://www.tcs.ifi.lmu.de/˜abel/MLFSigma.lhs, November 2004.
• [2] Abel, A.: Termination Checking with Types, RAIRO - Theoretical Informatics and Applications, 38(4), 2004, 277-319, Special Issue: Fixed Points in Computer Science (FICS'03).
• [3] Abel, A., Coquand, T.: Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs, Typed Lambda Calculi and Applications (TLCA 2005), Nara, Japan (P. Urzyczyn, Ed.), 3461, Springer-Verlag, April 2005.
• [4] Adams, R.: Decidable Equality in a Logical Framework with Sigma Kinds, 2001, Unpublished technical report, available on http://www.cs.man.ac.uk/˜radams/.
• [5] Adams, R.: Pure Type Systems with Judgemental Equality, Journal of Functional Programming, 16(2), 2006, 219-246.
• [6] Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics, North Holland, Amsterdam, 1984.
• [7] Benzmüller, C., Brown, C. E., Kohlhase, M.: Higher-Order Semantics and Extensionality, The Journal of Symbolic Logic, 69(4), December 2004, 1027-1088.
• [8] Coquand, T.: An Algorithm for Testing Conversion in Type Theory, in: Logical Frameworks (G. Huet, G. Plotkin, Eds.), Cambridge University Press, 1991, 255-279.
• [9] Coquand, T.: An Algorithm for Type-Checking Dependent Types, Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17-21, 1995, Kloster Irsee, Germany), 26, Elsevier Science, May 1996.
• [10] Coquand, T., Pollack, R., Takeyama, M.: A Logical Framework with Dependently Typed Records, Fundamenta Informaticae, 65(1-2), 2005, 113-134.
• [11] Davies, R., Pfenning, F.: Intersection Types and Computational Effects, Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), Montreal, Canada, September 2000.
• [12] Dybjer, P.: A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory, The Journal of Symbolic Logic, 65(2), 2000, 525-549.
• [13] Goguen, H.: Soundness of the Logical Framework for Its Typed Operational Semantics, Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings (J.-Y. Girard, Ed.), 1581, Springer-Verlag, 1999, ISBN 3-540-65763-0.
• [14] Goguen, H.: Justifying Algorithms for _ Conversion, Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings (V. Sassone, Ed.), 3441, Springer-Verlag, 2005, ISBN 3-540-25388-2.
• [15] Goguen, H.: A Syntactic Approach to Eta Equality in Type Theory, Proceedings of the 32nd ACMSIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005 (J. Palsberg,M. Abadi, Eds.), ACM, January 2005, ISBN 1-58113-830-X.
• [16] Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics, Journal of the Association of Computing Machinery, 40(1), January 1993, 143-184.
• [17] Harper, R., Pfenning, F.: On Equivalence and Canonical Forms in the LF Type Theory, ACM Transactions on Computational Logic, 6(1), 2005, 61-101, ISSN 1529-3785.
• [18] Joachimski, F., Matthes, R.: Short Proofs of Normalization, Archive of Mathematical Logic, 42(1), 2003, 59-87.
• [19] Klop, J. W.: Combinatory Reduction Systems, Mathematical Center Tracts, 27, 1980.
• [20] Lambek, J., Scott, P. J.: Introduction to Higher Order Categorical Logic, Cambridge University Press, New York, NY, USA, 1988, ISBN 0-521-35653-9.
• [21] Nordström, B., Petersson, K., Smith, J.: Martin-Löf's Type Theory, Handbook of Logic in Computer Science, 5, Oxford University Press, October 2000.
• [22] Pierce, B. C., Turner, D. N.: Local Type Inference, POPL 98: The 25TH ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California, 1998.
• [23] Pottier, F.: A modern eye on ML type inference: old techniques and recent developments, September 2005, Lecture notes for the APPSEM Summer School.
• [24] van Raamsdonk, F., Severi, P., Sørensen, M. H., Xi, H.: Perpetual Reductions in Lambda Calculus, Information and Computation, 149(2),March 1999, 173-225.
• [25] Sarnat, J.: LF_: The Metatheory of LF with _ types, 2004, Unpublished technical report, kindly provided by Carsten Schürmann.
• [26] Vanderwaart, J. C., Crary, K.: A Simplified Account of the Metatheory of Linear LF, Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh, 2002.
• [27] Vaux, L.: A type system with implicit types, June 2004, English version of his mémoire de maˆıtrise.
• [28] Vouillon, J.: Subtyping Union Types, Computer Science Logic, CSL'04 (J.Marcinkowski, A. Tarlecki, Eds.), 3210, Springer-Verlag, 2004.