The system \({\mathcal F}\) of variable types, fifteen years later
From MaRDI portal
Publication:1091379
DOI10.1016/0304-3975(86)90044-7zbMath0623.03013OpenAlexW2054969282WikidataQ56430852 ScholiaQ56430852MaRDI QIDQ1091379
Publication date: 1986
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(86)90044-7
direct limitpolymorphismsemanticsmodels of lambda calculusqualitative domainssystem F of variable typestype abstraction
Abstract data types; algebraic specification (68Q65) Categories admitting limits (complete categories), functors preserving limits, completions (18A35) Combinatory logic and lambda calculus (03B40)
Related Items
A computable expression of closure to efficient causation ⋮ The shuffle Hopf algebra and noncommutative full completeness ⋮ The interpretation of unsolvable λ-terms in models of untyped λ-calculus ⋮ Representations of algebraic domains and algebraic L-domains by information systems ⋮ Interpreting higher computations as types with totality ⋮ Order-incompleteness and finite lambda reduction models ⋮ Prime algebraicity ⋮ Intersection type assignment systems ⋮ Intersection-types à la Church ⋮ Least fixpoints of endofunctors of cartesian closed categories ⋮ Some monoidal closed categories of stable domains and event structures ⋮ The theory of semi-functors ⋮ From operational semantics to abstract machines ⋮ A higher-order calculus and theory abstraction ⋮ Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus ⋮ Rétractions et interprétation interne du polymorphisme : le problème de la rétraction universelle ⋮ Normal functors, power series and \(\lambda\)-calculus ⋮ A quantitative interpretation of Girard's System F ⋮ Categorical data types in parametric polymorphism ⋮ Comparing cubes of typed and type assignment systems ⋮ A new constructive logic: classic logic ⋮ Semantics of the second order lambda calculus ⋮ Semantics of quantum programming languages: Classical control, quantum control ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Games and full completeness for multiplicative linear logic ⋮ Projecting sequential algorithms on strongly stable functions ⋮ Glueing and orthogonality for models of linear logic ⋮ Visible acyclic differential nets. I: Semantics ⋮ A representation of L-domains by information systems ⋮ System ST toward a type system for extraction and proofs of programs ⋮ The Scott model of linear logic is the extensional collapse of its relational model ⋮ Internal models of system F for decompilation ⋮ Totality in arena games ⋮ A typed calculus based on a fragment of linear logic ⋮ Computation with classical sequents ⋮ Constructive system for automatic program synthesis ⋮ Alpha conversion, conditions on variables and categorical logic ⋮ Axioms and models of linear logic ⋮ An algebraic approach to stable domains ⋮ Coherence Spaces and Uniform Continuity ⋮ Incremental Update for Graph Rewriting ⋮ Between constructive mathematics and PROLOG ⋮ Inheritance as implicit coercion ⋮ Coherence spaces are untopological ⋮ Finite type structures within combinatory algebras ⋮ Stable neighbourhoods ⋮ Quantitative domains and infinitary algebras ⋮ Comparing models of the intensional typed \(\lambda\)-calculus ⋮ On maximal stable functions ⋮ Uniformity and the Taylor expansion of ordinary lambda-terms ⋮ Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves ⋮ Programs, Grammars and Arguments: A Personal View of some Connections between Computation, Language and Logic ⋮ Program development in constructive type theory ⋮ Information systems revisited -- the general continuous case ⋮ Equational theories for inductive types ⋮ Categorical models of polymorphism ⋮ The extended calculus of constructions (ECC) with inductive types ⋮ Linear logic, coherence and dinaturality ⋮ Stable domains are generalized topological spaces ⋮ Maximality and totality of stable functions in the category of stable bifinite domains ⋮ Preface to the special volume ⋮ Unnamed Item ⋮ Forcing in stable models of untyped \(\lambda\)-calculus ⋮ Total sets and objects in domain theory ⋮ Probabilistic coherence spaces as a model of higher-order probabilistic computation ⋮ A stable programming language ⋮ Linear logic ⋮ Logical Semantics for Stability ⋮ Strong storage operators and data types ⋮ Coherence and consistency in domains ⋮ Categories of embeddings ⋮ The semantics of second-order lambda calculus ⋮ Principal Types for Nominal Theories ⋮ Functorial polymorphism ⋮ A pluralist approach to the formalisation of mathematics ⋮ An algebraic generalization of Frege structures -- binding algebras ⋮ Typed lambda calculi and applications. 9th international conference, TLCA 2009, Brasilia, Brazil, July 1--3, 2009. Proceedings ⋮ Unnamed Item ⋮ Domain theoretic models of polymorphism ⋮ Building continuous webbed models for system F ⋮ Encoding types in ML-like languages ⋮ Dedekind completion as a method for constructing new Scott domains ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Quasi-coproducts and accessible categories with wide pullbacks ⋮ Parallel and serial hypercoherences ⋮ From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models ⋮ Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus ⋮ A relative PCF-definability result for strongly stable functions and some corollaries ⋮ The \(HOL\) logic extended with quantification over type variables ⋮ Relational model of second order linear logic ⋮ Historical introduction to ``Concrete domains by G. Kahn and G. D. Plotkin ⋮ The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus ⋮ Set-theoretical and other elementary models of the \(\lambda\)-calculus ⋮ A natural semantics of first-order type dependency ⋮ Retractions of dI-domains as a model for Type:Type ⋮ Full intuitionistic linear logic ⋮ CPO-models for second order lambda calculus with recursive types and subtyping ⋮ Relative definability of boolean functions via hypergraphs ⋮ \(QPC_ 2\): A constructive calculus with parameterized specifications ⋮ Coherent models of proof nets ⋮ An introduction to differential linear logic: proof-nets, models and antiderivatives ⋮ Execution time of λ-terms via denotational semantics and intersection types ⋮ Full abstraction and the Context Lemma (preliminary report) ⋮ Parametricity of extensionally collapsed term models of polymorphism and their categorical properties ⋮ Quantitative domains, groupoids and linear logic ⋮ Machine Deduction ⋮ Decomposition of domains ⋮ A monoidal closed category of event structures ⋮ Types, abstraction, and parametric polymorphism, part 2 ⋮ Mackey-complete spaces and power series – a topological model of differential linear logic ⋮ A linear/producer/consumer model of classical linear logic ⋮ POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE ⋮ Unnamed Item ⋮ Towards Lambda Calculus Order-Incompleteness ⋮ On the reification of semantic linearity ⋮ A \(\kappa\)-denotational semantics for map theory in ZFC+SI ⋮ Introduction to Type Theory ⋮ Unnamed Item ⋮ Lax familial representability and lax generic factorizations ⋮ On the construction of stable models of untyped \(\lambda\)-calculus ⋮ Pomset Logic
Cites Work
