Abstract
An untyped algorithm to test βη-equality for Martin-Löf’s Logical Framework with strong Σ -types is presented and proven complete using a model of partial equivalence relations between untyped terms.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abel, A., Coquand, T.: Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs (extended version). Tech. rep., Department of Computer Science, Chalmers, Göteborg, Sweden (2005)
Adams, R.: Decidable equality in a logical framework with sigma kinds, Unpublished note, see (2001), http://www.cs.man.ac.uk/~radams/
Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)
Coquand, T.: An algorithm for testing conversion in type theory. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 255–279. Cambridge University Press, Cambridge (1991)
Coquand, T.: An algorithm for type-checking dependent types. In: Möller, B. (ed.) MPC 1995. LNCS, vol. 947, pp. 167–177. Springer, Heidelberg (1996)
Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 105–119. Springer, Heidelberg (2003)
Goguen, H.: Soundness of the logical framework for its typed operational semantics. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 177–197. Springer, Heidelberg (1999)
Goguen, H.: Justifying algorithms for βη conversion. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 410–424. Springer, Heidelberg (2005) (To appear)
Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics. Journal of the Association of Computing Machinery 40(1), 143–184 (1993)
Harper, R., Pfenning, F.: On equivalence and canonical forms in the LF type theory. ACM Transactions on Computational Logic 6(1), 61–101 (2005)
Klop, J.W.: Combinatory reducion systems. Mathematical Center Tracts 27 (1980)
Nordström, B., Petersson, K., Smith, J.: Martin-löf’s type theory. In: Handbook of Logic in Computer Science, 5th edn. Oxford University Press, Oxford (2000)
Sarnat, J.: LFΣ: The metatheory of LF with Σ types. Unpublished technical report, kindly provided by Carsten Schürmann (2004)
Vaux, L.: A type system with implicit types, English version of his mémoire de maîtrise (2004)
Vanderwaart, J.C., Crary, K.: A simplified account of the metatheory of Linear LF. Tech. rep., Dept. of Comp. Sci., Carnegie Mellon (2002)
Vouillon, J.: Subtyping union types. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 415–429. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abel, A., Coquand, T. (2005). Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs. In: Urzyczyn, P. (eds) Typed Lambda Calculi and Applications. TLCA 2005. Lecture Notes in Computer Science, vol 3461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11417170_4
Download citation
DOI: https://doi.org/10.1007/11417170_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25593-2
Online ISBN: 978-3-540-32014-2
eBook Packages: Computer ScienceComputer Science (R0)