A formulation of the simple theory of types
From MaRDI portal
Publication:5777498
DOI10.2307/2266170zbMath0023.28901WikidataQ56001156 ScholiaQ56001156MaRDI QIDQ5777498
Publication date: 1940
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2266170
Related Items
From operational semantics to abstract machines, Hoare logic for Java in Isabelle/HOL, The Impact of the Lambda Calculus in Logic and Computer Science, Programs, Grammars and Arguments: A Personal View of some Connections between Computation, Language and Logic, Alonzo church:his life, his work and some of his miracles, Russell's 1903 - 1905 Anticipation of the Lambda Calculus, Mechanizing Nonstandard Real Analysis, Proof normalization modulo, Completeness and Categoricity. Part I: Nineteenth-century Axiomatics to Twentieth-century Metalogic, Equivalences between logics and their representing type theories, Canonical typing and ∏-conversion in the Barendregt Cube, Unnamed Item, Unnamed Item, Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism, Why Sets?, On cubism, Semantics of constructions. I: The traditional approach, Remark on complete interpretations by models, Using typed lambda calculus to implement formal systems on a machine, Expressing combinatory reduction systems derivations in the rewriting calculus, On connections and higher-order logic, Formalizing non-interference for a simple bytecode language in Coq, A compact representation of proofs, Intuitionist type theory and foundations, A completeness theorem for the general interpreted modal calculus MC**nu of A. Bressan, Lambek calculus with restricted contraction and expansion, Types with intersection: An introduction, Expressibility of propositions in \(L_\mu\)-languages, Adverbs and events, A unification algorithm for typed \(\bar\lambda\)-calculus, The \(HOL\) logic extended with quantification over type variables, Lazy techniques for fully expansive theorem proving, Mechanizing some advanced refinement concepts, Implementing tactics and tacticals in a higher-order logic programming language, What holds in a context?, A type-theoretical alternative to ISWIM, CUCH, OWHY, IMPS: An interactive mathematical proof system, Annotations in formal specifications and proofs, Using tactics to reformulate formulae for resolution theorem proving, Semantic bootstrapping of type-logical grammar, TPS: A theorem-proving system for classical type theory, Modèles à variables de différentes sortes pour les logiques modales \(M\) ou \(S5\), A modern elaboration of the ramified theory of types, A note on the use of lamda conversion in generalized phrase structure grammars, A new type assignment for λ-terms, Über Interpretationen der Prädikatenkalküle Höherer Stufe, Symmetry and Paradox, In the Search of a Naive Type Theory, Computation with classical sequents, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, THF0 – The Core of the TPTP Language for Higher-Order Logic, Querying and Merging Heterogeneous Data by Approximate Joins on Higher-Order Terms, A Brief Overview of HOL4, Hoare type theory, polymorphism and separation, A Clausal Approach to Proof Analysis in Second-Order Logic, Formal verification of tail distribution bounds in the HOL theorem prover, Unnamed Item, Automatic theorem proving. II, A relational formulation of the theory of types, Unnamed Item, Unnamed Item, Alonzo Church's Contributions to Philosophy and Intensional Logic
Cites Work
