Abstract
The paper discusses the setting of type theory and proposes a uniform framework for disciplines of declarations and types. The framework combines fundamental concepts found in the setting of type theory and supports both its denotational and its constructive view. In the denotational view ε-structures are introduced as semantic models and in the constructive view the general forms of judgements and rules are given. Finally applications arc discussed which build on the ideas of this framework, namely models of untyped λ-calculus which truly solve the equation of reflexive domains, and εT-logic, a first-order theory of propositions with selfrcfcrcncc and imprcdicative quantification allowing for intcnsional models of truth.
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
Aczel, P.: Non-Wellfoundcd Sets, CSLI Lecture Notes 14, 1988
Barendregt, H.: Introduction to Generalized Type Systems, Tech. Report 90-8, Univ. of Nijmcgen, 1990.
Ballmann, S., Dunker, G.: Entwurf und Implementierung für den Kalkül getypter Deklarationen, students thesis, Fachbereich 20, TU Berlin 1991
Bläsius, K.H., Hcdtstück, U., Rollinger, C.R. (eds): Sorts and Types in Artificial Intelligence, LNAI 418, Springer, 1990
Curry, H.B., Fcys, R.: Combinatory Logic, North Holland, 1958
Church, A.: A formulation of the simple Theory of Types, J. Symb. Log. 5, 1940, 56–68
Coquand, Th., Huet, G.: The Calculus of Constructions, Information and Computation 76, 2/3, 1988, 95–120
Coquand, Th.: Une théorie des constructions, Thèse, Université Paris VII, 1985
Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1, Springer-Verlag, 1985
Fraenkel, A.A., Bar-Hillel, Y., Levy, A.: Foundations of Set Theory, North-Holland, 1984
Gentzen, G.: The collected Papers of Gerhard Gcntzcn. ed E. Szabo, North Holland, 1969
Girard, J.Y.: Une extension de l'interprétation de Gödel à l'analyse et son application à r élimination des conpures dans l'analyse et dans le théorie des types, Proc. of the Zud Scandinavian Logic Symposium (ed. LE. Fenstad), North Holland, 1971, 63–92
Herbrand, J.: Investigations in Proof Theory (1930) in: Logical Writings, ed. W.D. Goldfarb, Reidel, 1971
Higgins, P.J.: Algebra with a scheme of operators, Mathematische Nachrichten, 27, 1963, 115–132
Howard, W.A.: The formulae-as-Types notion of construction, in: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, ed. J.P. Seklin and J.R. Hindley, Academic Press, 1980, 479–490
Luo, Z.: An Extended Calculus of Constructions, Dept. of Comp. Science, Univ. of Edinburgh, 1990
Meyer, A.R.: What is a model of Lambda Calculus? in: Information and Control 52, 1982, 87–122
Milner, R.: A Theory of Type Polymorphism in Programming, J.C.S.S. 17, 1978, 384–375
Martin-Löf, P.: A Theory or Types, Report 71-3, Dept. of Math., Univ. of Stockholm, 1971
Martin-Löf, P.: Constructive Mathematics and Computer Programming, Logic, Methodology and Philosophy of Science 6, 1980, 153–175
Martin-Löf, P.: Intuitionislic Type Theory, Bibliopolis, 1984
Mahr, B., Sträter, W., Um bach, C.: Fundamentals of a Theory of Types and Declarations, KIT-Rcport 82, TU Berlin, Fachbereich 20, 1990
Nordström, B.: Programming in Constructive Set Theory: Some Examples. Proc. ACM Conf. of Funct. Prog. Lang. and Comp. Arch., ACM, 1981, 141–154
Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löfs' Type Theory, Clarendon Press, 1990
Pooyan, L.: ε-structures as Semantic Models of the λ-calculus, Diploma Thesis, Fachbereich Informatik, TU Berlin, 1992
Quinc, W.O.: Mengenlehre und ihre Logik, Vieweg, 1973, First published in 1963
Reynolds, J.C.: Towards a Theory of Type Structure, LNCS 19, Springer-Verlag, 1974,408–425
Russell, B.: Mathematical Logic as based on the theory of types, Am. J. Math. 30, 1908, 222–262
Sträter, W.: εT Eine Logik erster Stufe mit Selbstreferenz und totalem Wahrheilsprädikal, KIT-Rcporl 98, TU Berlin, Fachbereich 20, 1992
Sträter, W.: Internal notes on non wcllfounded sets, Fachbereich 20, TU Berlin, 1992
Thompson, S.: Type Theory and Functional Programming, Addison-Wesley, 1991
Umbach, C.: A standard discipline in the calculus of declarations. Internal notes, Fachbereich 20, TU Berlin, 1991
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mahr, B. (1993). Applications of type theory. In: Gaudel, M.C., Jouannaud, J.P. (eds) TAPSOFT'93: Theory and Practice of Software Development. CAAP 1993. Lecture Notes in Computer Science, vol 668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56610-4_75
Download citation
DOI: https://doi.org/10.1007/3-540-56610-4_75
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56610-6
Online ISBN: 978-3-540-47598-9
eBook Packages: Springer Book Archive