Abstract
A type-theoretic framework for formal reasoning with different logical foundations is introduced and studied. With logic-enriched type theories formulated in a logical framework, it allows various logical systems such as classical logic as well as intuitionistic logic to be used effectively alongside inductive data types and type universes. This provides an adequate basis for wider applications of type theory based theorem proving technology. Two notions of set are introduced in the framework and used in two case studies of classical reasoning: a predicative one in the formalisation of Weyl’s predicative mathematics and an impredicative one in the verification of security protocols.
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
Aczel, P., Gambino, N.: Collection principles in dependent type theory. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, Springer, Heidelberg (2002)
Agda proof assistant (2000), http://www.cs.chalmers.se/~catarina/agda
Adams, R., Luo, Z.: Weyl’s predicative classical mathematics as a logic-enriched type theory. In: TYPES 2006 (2006) (submitted)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proc. of the Royal Society of London 426, 233–271 (1989)
Constable, R., et al.: Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs (1986)
Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76(2/3) (1988)
Callaghan, P.C., Luo, Z.: An implementation of typed LF with coercive subtyping and universes. J. of Automated Reasoning 27(1), 3–27 (2001)
The Coq Development Team. The Coq Proof Assistant Reference Manual (Version 8.0), INRIA (2004)
Feferman, S.: The significance of Hermann Weyl’s Das Kontinuum. In: Hendricks, V., et al. (eds.) Proof Theory (2000)
Feferman, S.: Predicativity. In: Shapiro, S. (ed.) The Oxford Handbook of Philosophy of Mathematics and Logic, Oxford Univ Press, Oxford (2005)
Gambino, N., Aczel, P.: The generalised type-theoretic interpretation of constructive set theory. J. of Symbolic Logic 71(1), 67–103 (2006)
Gonthier, G.: A computer checked proof of the four colour theorem (2005)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, Springer, Heidelberg (1996)
Luo, Z., Pollack, R.: LEGO Proof Development System: User’s Manual. LFCS Report ECS-LFCS-92-211, Dept of Computer Science, Univ of Edinburgh (1992)
Luo, Z.: Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Oxford (1994)
Luo, Z.: PAL + : a lambda-free logical framework. Journal of Functional Programming 13(2), 317–338 (2003)
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)
Magnusson, L., Nordström, B.: The ALF proof editor and its proof engine. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, Springer, Heidelberg (1994)
Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, Oxford (1990)
Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Comm. of the ACM 21(12), 993–999 (1978)
Paulson, L.: Isabelle: a generic theorem prover. LNCS, vol. 828. Springer, Heidelberg (1994)
Paulson, L.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85–128 (1998)
Paulson, L.: Proving security protocols correct. In: LICS (1999)
Simpson, S.: Subsystems of Second-Order Arithmetic. Springer, Heidelberg (1999)
Smith, J.: The independence of Peano’s fourth axiom from Martin-Löf’s type theory without universes. Journal of Symbolic Logic 53(3) (1988)
Weyl, H.: The Continuum: a critical examination of the foundation of analysis. Dover Publ., (English translation of Das Kontinuum, 1918) (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Luo, Z. (2007). A Type-Theoretic Framework for Formal Reasoning with Different Logical Foundations. In: Okada, M., Satoh, I. (eds) Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues. ASIAN 2006. Lecture Notes in Computer Science, vol 4435. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77505-8_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-77505-8_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77504-1
Online ISBN: 978-3-540-77505-8
eBook Packages: Computer ScienceComputer Science (R0)