Intensional interpretations of functionals of finite type I
From MaRDI portal
Publication:5561939
DOI10.2307/2271658zbMath0174.01202OpenAlexW2149837936WikidataQ56532580 ScholiaQ56532580MaRDI QIDQ5561939
Publication date: 1967
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2271658
Related Items
On the Versatility of Open Logical Relations, Semantic analysis of normalisation by evaluation for typed lambda calculus, Some lambda calculi with categorical sums and products, (Head-)normalization of typeable rewrite systems, Unnamed Item, Strong normalisation for the linear term calculus, The metatheory of UTT, Unnamed Item, A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go, Semantic preservation for a type directed translation scheme of Featherweight Go, A Formal Proof of the Strong Normalization Theorem for System T in Agda, Adding Negation to Lambda Mu, POPLMark reloaded: Mechanizing proofs by logical relations, The conservation theorem for differential nets, Canonicity and homotopy canonicity for cubical type theory, Unnamed Item, A system of abstract constructive ordinals, On n-quantifier induction, Implicative algebras: a new foundation for realizability and forcing, An analysis of the Core-ML language: Expressive power and type reconstruction, A confluent reduction for the λ-calculus with surjective pairing and terminal object, POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE, Approximation and normalization results for typeable term rewriting systems, Two different strong normalization proofs?, Proof Terms for Generalized Natural Deduction, Proof normalization modulo, A generalization of the Takeuti–Gandy interpretation, Simplified Reducibility Proofs of Church-Rosser for β- and βη-reduction, Introduction to Type Theory, Unnamed Item, A metalanguage for guarded iteration, Unnamed Item, Inductive-data-type systems, Mechanizing proofs with logical relations – Kripke-style, Prawitz, Proofs, and Meaning, Explaining Deductive Inference, First-Order Logic Without Bound Variables: Compositional Semantics, On the Computability of the Fan Functional, Cartesian cubical computational type theory: Constructive reasoning with paths and equalities, Normalization by Evaluation for Typed Weak lambda-Reduction, Unnamed Item, ETA-RULES IN MARTIN-LÖF TYPE THEORY, Gödel and Intuitionism, An Approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited, Higher order functions and Brouwer’s thesis, Quantifier elimination and parametric polymorphism in programming languages, The complexity of type inference for higher-order typed lambda calculi, Taming the Merge Operator, Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation, A characterization of F-complete type assignments, On the implementation of abstract data types by programming language constructs, Intersection types for explicit substitutions, Coq formalization of the higher-order recursive path ordering, Inductive Beluga: Programming Proofs, Productivity of stream definitions, Intersection type assignment systems, Strong normalization for non-structural subtyping via saturated sets, Normalization results for typeable rewrite systems, Strong normalization from weak normalization in typed \(\lambda\)-calculi, Type theories, normal forms, and \(D_{\infty}\)-lambda-models, A strong normalization result for classical logic, Call-by-push-value: Decomposing call-by-value and call-by-name, A herbrandized functional interpretation of classical first-order logic, Higher-order subtyping and its decidability, Strong normalisation in the \(\pi\)-calculus, Linear Läuchli semantics, Polymorphic extensions of simple type structures. With an application to a bar recursive minimization, Size-based termination of higher-order rewriting, Termination of system \(F\)-bounded: A complete proof, Strong normalization and typability with intersection types, Combinatorial realizability models of type theory, Semantic types and approximation for Featherweight Java, Intuitionistic completeness of first-order logic, Nominal abstraction, Canonicity and normalization for dependent type theory, Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility, Elementary Proof of Strong Normalization for Atomic F, Typed operational semantics for higher-order subtyping., Setting the facts straight, The Scott model of linear logic is the extensional collapse of its relational model, An abstract Church-Rosser theorem. II: Applications, A mathematical semantics for a nondeterministic typed lambda-calculus, Identity and intensionality in univalent foundations and philosophy, A rationale for conditional equational programming, Program equivalence in a simple language with state, Binary trees as a computational framework, The Abella Interactive Theorem Prover (System Description), On strong normalization and type inference in the intersection type discipline, The heart of intersection type assignment: Normalisation proofs revisited, Linear logical relations and observational equivalences for session-based concurrency, Polymorphic rewriting conserves algebraic strong normalization, About primitive recursive algorithms, Behavioural inverse limit \(\lambda\)-models, Partial inductive definitions, Enhancing dependency pair method using strong computability in simply-typed term rewriting, Term-space semantics of typed lambda calculus, Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves, Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming, Iteration and labelled iteration, Strong normalization through intersection types and memory, An intuitionistic theory of types with assumptions of high-arity variables, Structural recursion with locally scoped names, Functional interpretations of feasibly constructive arithmetic, Constructing type systems over an operational semantics, Strong normalization from an unusual point of view, Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi, Cut-elimination in the strict intersection type assignment system is strongly normalizing, Typing termination in a higher-order concurrent imperative language, An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus, A sequent calculus for type assignment, On the proof-theoretic foundation of general definition theory, Validity concepts in proof-theoretic semantics, A categorical construction for the computational definition of vector spaces, Polymorphic lambda calculus: The Church-Rosser property, Normalization and excluded middle. I, The harmony of identity, The Attributed Pi-Calculus with Priorities, Reasoning in Abella about Structural Operational Semantics Specifications, A Context-based Approach to Proving Termination of Evaluation, Abstracting models of strong normalization for classical calculi, Unnamed Item, N. G. de Bruijn's contribution to the formalization of mathematics, Theory of proofs (arithmetic and analysis), A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++, Implementing a normalizer using sized heterogeneous types, Big-step normalisation, A unary representation result for system \(T\), Curry-Howard-Lambek correspondence for intuitionistic belief, Typing and computational properties of lambda expressions, System \(T\), call-by-value and the minimum problem, Infinite \(\lambda\)-calculus and types, Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions, Intersection Types for the Resource Control Lambda Calculi, Automated higher-order complexity analysis, Canonicity for cubical type theory, Perpetual reductions in \(\lambda\)-calculus, Cut-elimination for a logic with definitions and induction, Strongly Normalising Cut-Elimination with Strict Intersection Types, Reducibility, Reduction of finite and infinite derivations, Typing untyped \(\lambda\)-terms, or reducibility strikes again!, \({\mathcal M}^\omega\) considered as a programming language, Normalization, approximation, and semantics for combinator systems, Dependent types with subtyping and late-bound overloading, Conservation and uniform normalization in lambda calculi with erasing reductions, On the Convergence of Reduction-based and Model-based Methods in Proof Theory, A uniform semantic proof for cut-elimination and completeness of various first and higher order logics., A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
Cites Work
