A formulation of the simple theory of types

Keywords

Ackermann function, Type theory, Simple (philosophy), Symbol (formal), Type (biology)

References

• Über die Bausteine der mathematischen LogikM. Schönfinkel — 1924
• Abriss der Logistik: Mit Besonderer Berücksichtigung der Relationstheorie und Ihrer AnwendungenRudolf Carnap — 1929
• Grundzüge der theoretischen LogikDavid Hilbert, W. Ackermann — 1928
• Axiomatische Untersuchung des Aussagen-Kalkuls der “Principia Mathematica”Paul Bernays — 1926
• A Theory of Positive Integers in Formal Logic. Part IIS. C. Kleene — 1935
• Grundlagen der MathematikH. G. F. — 1934
• Mathematical Logic as Based on the Theory of TypesBertrand Russell — 1908
• Bertrand Russell. Mathematical logic as based on the theory of types. A reprint of the first five sections of 11116. Contemporary readings in logical theory, edited by Irving M. Copi and James A. Gould, The Macmillan Company, New York, and Collier-Macmillan Limited, London, 1967, pp. 135–153.Alonzo Church — 1974

Cited by

• The Type System of a Higher-Order Logic Programming LanguageGopalan Nadathur, Frank Pfenning — 1992
• Test generation and animation based on object-oriented specifications. (Génération de tests et animation à partir de spécifications orientées objet)Matthias P. Krieger, WOLFF, Burkhart — 2011
• Exploiting PSL standard assertions in a theorem-proving-based verification environmentAnli He, Parija Sule, Young‐Sik Kim — 2005
• Formalizing abstraction mechanisms for hardware verification in higher order logicThomas F. Melham — 1990
• Mechanising Hilbert's Foundations of Geometry in IsabellePhil Scott — 2008
• Higher order logicDaniël Leivant — 1994
• Theoretical Foundations for Practical 'Totally Functional Programming'Colin Kemp — 2007
• From fuzzy type theory to fuzzy intensional logicVilém Novák — 2003
• On the Translation of Higher-Order Problems into First-Order LogicManfred Kerber — 1994
• Institution-independent Model TheoryRăzvan Diaconescu, Vasyukov, Vladimir, Schröder-Heister, Peter — 2025
• Coding Binding and Substitution Explicitly in IsabelleChristopher Owens — 2003
• SOFSEM 2002: Theory and Practice of InformaticsSOFSEM 2002 Milovice, Grosky, William I. — 2002
• Polynomial Representations and Primordial Self-Similarity in the Hierarchy of Universal LexiconsT. E. Raptis — 2011
• Criss-Crossing A PHILOSOPHICAL LANDSCAPE. Essays on Wittgensteinian Themes. Dedicated to Brian McGuinness.Joachim Schulte, Göran Sundholm — 1992
• La sémantique dans les grammaires d’interactionGuy Perrier — 2004
• Un système X Raisonner formellement sur les programmes MLSylvain Baro, Pascal Manoury — 2003
• Types and verification for infinite state systemsGavin Mendel-Gleason — 2012
• HOL-lambdasigma: An Intentional First-Order Expression of Higher-Order LogicGilles Dowek, Thérèse Hardin, Claude Kirchner — 1999
• Formal mechanization of device interactions with a process algebraE. Thomas Schubert, Karl Levitt, Gerald C. Cohen — 1992
• Presupposition and partiality: Back to the futureDavid Beaver, Emiel Krahmer — 1998

Related papers

• The complexity of computing partial sums off-lineBernard Chazelle, Burton Rosenberg — 1991
• General recursion via coinductive typesVenanzio Capretta — 2005
• A Formal Logic for Formal Category TheoryMax S. New, Daniel R. Licata — 2023
• Partial Objects in Type TheoryScott F. Smith — 1988
• Remarks on Martin-Löf's partial type theoryErik Palmgren, V. Stoltenberg-Hansen — 1992