Logical relations and the typed λ-calculus
From MaRDI portal
Publication:3724297
DOI10.1016/S0019-9958(85)80001-2zbMath0594.03006MaRDI QIDQ3724297
Publication date: 1985
Published in: Information and Control (Search for Journal in Brave)
Related Items
Logical relations and parametricity -- a Reynolds programme for category theory and programming languages, Semantic analysis of normalisation by evaluation for typed lambda calculus, Constructive set theoretic models of typed combinatory logic, Specification and verification of object-oriented programs using supertype abstraction, Fully abstract translations between functional languages, An intersection problem for finite automata, Linear Läuchli semantics, Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels, Intuitive counterexamples for constructive fallacies, The behavior-realization adjunction and generalized homomorphic relations, 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, Typed homomorphic relations extended with subtypes, Types, abstraction, and parametric polymorphism, part 2, Relative full completeness for bicategorical Cartesian closed structure, Linear logical relations and observational equivalences for session-based concurrency, Polymorphic rewriting conserves algebraic strong normalization, Logical relations for monadic types, Behavioural inverse limit \(\lambda\)-models, A characterization of lambda definability in categorical models of implicit polymorphism, Selective strictness and parametricity in structural operational semantics, inequationally, Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves, An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras, A verified framework for higher-order uncurrying optimizations, A generalization of the Takeuti–Gandy interpretation, Finitary PCF is not decidable, Unnamed Item, A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++, An algebraic generalization of Frege structures -- binding algebras, Unary PCF is decidable, On abstraction and the expressive power of programming languages, Reducibility, Safe recursion with higher types and BCK-algebra, Term-generic logic, Relational interpretations of recursive types in an operational setting., Prelogical relations, Syntactic Logical Relations for Polymorphic and Recursive Types, Program equivalence in linear contexts, Kripke-style models for typed lambda calculus, Taming the Merge Operator
