This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
P. Aczel. A notion of class for theory development in algebra in a predicative type theory. Talk presented at the Workshop on Types for Proofs and Programs, June 1994.
H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3. Oxford science publications, 1994.
Henk Barendregt. The quest of correctness. Images of SMC research, Stichting Mathematisch Centrum, P.O. Box 94079, 1090 GB Amsterdam, 39–58.
A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.
T. Coquand. Metamathematical Investigations of a Calculus of Constructions. In P. Odifreddi, editor, Logic and Computer Science, volume 31 of The APIC series, pages 91–122. Academic Press, 1990.
T. Coquand. On the analogy between propositions and types. In G. Huet, editor, Logical Foundations of Functional Programming, pages 399–417. Addison-Wesley, 1990.
Th. Coquand and G. Huet. Constructions: A higher order proof system for mechanizing mathematics. In EUROCAL'85, volume 203 of LNCS, Linz, 1985. Springer-Verlag.
C. Cornes and D. Terrasse. Automatizing Inversion Predicates in Coq. In Workshop on Types for Proofs on Programs, number 1152 in LNCS. Springer-Verlag, 1995.
EC Types Working Group. First Workshop on Formal Topology, Padova, October 1997.
E. Giménez. An application of co-Inductive types in Coq: verification of the Alternating Bit Protocol. In Workshop on Types for Proofs and Programs, number 1158 in LNCS, pages 135–152. Springer-Verlag, 1995.
J.-Y. Girard. Proceedings of the 2nd scandinavian logic symposium. In J.E. Fenstad, editor, Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la téorie des types, pages 63–92. North-Holland, 1971.
J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1989.
M.J. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF, volume 78 of LNCS. Springer-Verlag, 1979.
M.J.C. Gordon and T. F. Melham. Introduction to HOL. A theorem proving environment for higher order logic. University of Cambridge, 1993.
L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-Checking a Data Link Protocol. In Henk Barendregt, Tobias Nipkow, editor, Workshop on Types for Proofs and Programs, volume 806 of LNCS, pages 127–165. Springer-Verlag, 1993.
A. Heyting. Intuitionism: An Introduction. North-Holland, 1971.
W.A. Howard. The formulae-as-types notion of constructions. In J.P. Seldin and J.R. Hindley, editors, to H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980. Unpublished 1969 Manuscript.
G. Huet and G. Plotkin, editors. Logical Frameworks. Cambridge University Press, May 1991.
Z. Luo. Computation and Reasoning: A Type Theory for Computer Science, volume 11 of International Series of Monographs on Computer Science. Oxford Science Publications, 1994.
L. Magnusson. The implementation of ALF-a Proof Editor based on Martin-Löf's Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers University of Göteborg, 1994.
C. McLarty. Elementary Categories, Elementary Toposes. Oxford University Press, 1992.
P.-A. Melliès. Typed γ-calculi with explicit substitutions may not terminate. In Typed Lambda Calculi and Applications, number 902 in LNCS. Second International Conference TLCA'95, Springer-Verlag, 1995.
P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer, editors. Selected Papers on Automath. North-Holland, 1994.
T. Nipkow, and K. Slind. IO Automata in Isabelle/HOL. In P Dybjer, B. Nordström, and J. Smith, editors, Workshop on Types for Proofs and Programs, number 996 in LNCS, pages 101–119. Springer-Verlag, 1994.
B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf's Type Theory: An Introduction, volume 7 of International Series of Monographs on Computer Science. Oxford Science Publications, 1990.
S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes in Computer Science, pages 411–414, New Brunswick, NJ, July/August 1996. Springer-Verlag.
P. Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, 1984.
C. Paulin-Mohring and B. Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15:607–640, 1993.
L. Paulson. Set theory for verification: from foundations to functions. Journal of Automatic Reasoning, 11(2):353–389, 1993.
L. Paulson. The Isabelle reference manual. Technical Report 283, Computer Laboratory, University of Cambridge, 1993.
L. Paulson. Set theory for verification: induction and recursion. Journal of Automatic Reasoning, 15(3), 1995.
A. Ranta. Type-theoretical grammar. Oxford: Clarendon, 1994.
P. Rudnicki. An overview of the Mizar project, 1992.
G. Sambin and J. Smith, editors. Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998.
A. Whitehead and B. Russel. Principia Mathematica. Cambridge University Press, 1910.
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
(1998). Introduction. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0097783
Download citation
DOI: https://doi.org/10.1007/BFb0097783
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65137-6
Online ISBN: 978-3-540-49562-8
eBook Packages: Springer Book Archive