Abstract
We present a method for defining logical frameworks as a collection of features which are defined and behave independently of one another. Each feature is a set of grammar clauses and rules of deduction such that the result of adding the feature to a framework is a conservative extension of the framework itself. We show how several existing logical frameworks can be so built, and how several much weaker frameworks defined in this manner are adequate for expressing a wide variety of object logics.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Pientka, B., Pfenning, F.: Optimizing higher-order pattern unification (2003)
Jojgov, G.I.: Holes with binding power. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 162–181. Springer, Heidelberg (2003)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. In: Proceedings 2nd Annual IEEE Symp. on Logic in Computer Science, LICS 1987, Ithaca, NY, USA, June 22-25, pp. 194–204. IEEE Computer Society Press, New York (1987)
Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf’s Type Theory: an Introduction. Oxford University Press, Oxford (1990)
Nederpelt, R.P., Geuvers, J.H., Vrijer, R.C.D. (eds.): Selected Papers on AUTOMATH. Studies in Logic and the Foundations of Mathematics, vol. 133. North-Holland, Amsterdam (1994)
Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems:introduction and survey. Theoretical Computer Science 121, 279–308 (1993)
Ghani, N.: Eta-expansions in dependent type theory — the calculus of constructions. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 164–180. Springer, Heidelberg (1997)
Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science, vol. 11. Oxford University Press, Oxford (1994)
Luo, Z.: PAL+: a lambda-free logical framework. Journal of Functional Programming 13, 317–338 (2003)
Levin, M.Y., Pierce, B.C.: Tinkertype: A language for playing with formal systems. Technical report (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Adams, R. (2004). A Modular Hierarchy of Logical Frameworks. In: Berardi, S., Coppo, M., Damiani, F. (eds) Types for Proofs and Programs. TYPES 2003. Lecture Notes in Computer Science, vol 3085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24849-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-24849-1_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22164-7
Online ISBN: 978-3-540-24849-1
eBook Packages: Springer Book Archive