A formulation of the simple theory of types
From MaRDI portal
Publication:5777498
DOI10.2307/2266170zbMath0023.28901OpenAlexW1996404651WikidataQ56001156 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
Applications of type theory, Unnamed Item, A restricted form of higher-order rewriting applied to an HDL semantics, From operational semantics to abstract machines, Every Elementary Higher Topos has a Natural Number Object, Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach, Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types, Formalizing Ordinal Partition Relations Using Isabelle/HOL, Encoding natural semantics in Coq, Unnamed Item, A Survey of the Proof-Theoretic Foundations of Logic Programming, Correctness of procedure representations in higher-order assembly language, Equivalences between logics and their representing type theories, Hoare logic for Java in Isabelle/HOL, The Syntax of Many-Valued Relations, On cubism, Unnamed Item, The Impact of the Lambda Calculus in Logic and Computer Science, Canonical typing and ∏-conversion in the Barendregt Cube, Higher-Order Tarski Grothendieck as a Foundation for Formal Proof., A logical framework combining model and proof theory, Programs, Grammars and Arguments: A Personal View of some Connections between Computation, Language and Logic, On sets, types, fixed points, and checkerboards, Proof search with set variable instantiation in the Calculus of Constructions, Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them, Proof normalization modulo, Alonzo church:his life, his work and some of his miracles, Semantics of constructions. I: The traditional approach, A generalization of the Takeuti–Gandy interpretation, Proof Checking and Logic Programming, Simplified Reducibility Proofs of Church-Rosser for β- and βη-reduction, Specifying Proof Systems in Linear Logic with Subexponentials, A case-study in algebraic manipulation using mechanized reasoning tools, Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism, Introduction to Type Theory, A formal proof of the expressiveness of deep learning, Parsing and Disambiguation of Symbolic Mathematics in the Naproche System, Why Sets?, THE CONCEPTHORSEIS A CONCEPT, Proof Theory of Constructive Systems: Inductive Types and Univalence, Predicativity and Feferman, Completeness and Categoricity. Part I: Nineteenth-century Axiomatics to Twentieth-century Metalogic, Russell's 1903 - 1905 Anticipation of the Lambda Calculus, Two-level Lambda-calculus, Completeness: from Gödel to Henkin, Remark on complete interpretations by models, Unnamed Item, Towards the Formal Reliability Analysis of Oil and Gas Pipelines, Alonzo Church's Contributions to Philosophy and Intensional Logic, LAMBDA-REPRESENTABLE FUNCTIONS OVER TERM ALGEBRAS, Mechanizing Nonstandard Real Analysis, Category theory, logic and formal linguistics: some connections, old and new, Towards Logical Frameworks in the Heterogeneous Tool Set Hets, Annotations in formal specifications and proofs, Proving fairness and implementation correctness of a microkernel scheduler, Intertheoretic reduction, confirmation, and Montague's syntax-semantics relation, Probabilistic modelling, inference and learning using logical theories, Coq formalization of the higher-order recursive path ordering, A Bit of History Related to Logic Based on Equality, Henkin on Completeness, Assignment Calculus: A Pure Imperative Language, Meaning and computing: two approaches to computable propositions, HOL Light: An Overview, A compact representation of proofs, Expressing combinatory reduction systems derivations in the rewriting calculus, Semantics, calculi, and analysis for object-oriented specifications, A two-level logic approach to reasoning about computations, Functorial semantics of first-order views, Type theory and formalisation of mathematics, Homotopy type theory and Voevodsky’s univalent foundations, A new type assignment for λ-terms, Using tactics to reformulate formulae for resolution theorem proving, TPS: A theorem-proving system for classical type theory, Structured derivations: a unified proof style for teaching mathematics, Carnap, Goguen, and the hyperontologies: logical pluralism and heterogeneous structuring in ontology design, In the Search of a Naive Type Theory, Embedding and automating conditional logics in classical higher-order logic, Unnamed Item, Quantified multimodal logics in simple type theory, Intuitionist type theory and foundations, Unnamed Item, Über Interpretationen der Prädikatenkalküle Höherer Stufe, Semantics of \textsc{OpenMath} and \textsc{MathML3}, On connections and higher-order logic, Computation with classical sequents, Analytic tableaux for higher-order logic with choice, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, The Cooper storage idiom, A completeness theorem for the general interpreted modal calculus MC**nu of A. Bressan, Grammar induction by unification of type-logical lexicons, Automatic theorem proving. II, Comorphisms of structured institutions, Bounded memory Dolev-Yao adversaries in collaborative systems, A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms, Combining and automating classical and non-classical logics in classical higher-order logics, 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, Formalizing non-interference for a simple bytecode language in Coq, Hoare type theory, polymorphism and separation, A relational formulation of the theory of types, Lambek calculus with restricted contraction and expansion, Types with intersection: An introduction, Using typed lambda calculus to implement formal systems on a machine, A simple proof that super-consistency implies cut elimination, A higher-order theory of presupposition, Unnamed Item, Natural language inference in Coq, Expressibility of propositions in \(L_\mu\)-languages, A note on the use of lamda conversion in generalized phrase structure grammars, Adverbs and events, A framework for proof systems, A unification algorithm for typed \(\bar\lambda\)-calculus, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, Semantic bootstrapping of type-logical grammar, CERES in higher-order logic, Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners), A Clausal Approach to Proof Analysis in Second-Order Logic, Formal verification of tail distribution bounds in the HOL theorem prover, Unnamed Item, A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, Filter quotients and non-presentable \((\infty,1)\)-toposes, Automating free logic in HOL, with an experimental application in category theory, Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics, Extracting Higher-Order Goals from the Mizar Mathematical Library, Modèles à variables de différentes sortes pour les logiques modales \(M\) ou \(S5\), A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality, Validating QBF Validity in HOL4, Agent-Based HOL Reasoning, Kripke Semantics for Martin-Löf’s Extensional Type Theory, Local Theory Specifications in Isabelle/Isar, Formalising foundations of mathematics, Monadic Sequence Testing and Explicit Test-Refinements, ON THE TERMINATION OF RUSSELL’S DESCRIPTION ELIMINATION ALGORITHM, Adapting functional programs to higher order logic, Supra-logic: using transfinite type theory with type variables for paraconsistency, Proceeding in Abstraction. From Concepts to Types and the Recent Perspective on Information, Using theorem proving to verify expectation and variance for discrete random variables, A modern elaboration of the ramified theory of types, Proofs for free, A proof theory for model checking, The \(HOL\) logic extended with quantification over type variables, Lazy techniques for fully expansive theorem proving, Mechanizing some advanced refinement concepts, A formalization of the Smith normal form in higher-order logic, Implementing tactics and tacticals in a higher-order logic programming language, What holds in a context?, Symmetry and Paradox, A type-theoretical alternative to ISWIM, CUCH, OWHY, IMPS: An interactive mathematical proof system, Why ramify?
Cites Work
