Logical relations and the typed λ-calculus
From MaRDI portal
Recommendations
Cited in
(72)- Typed homomorphic relations extended with subtypes
- A contextual formalization of structural coinduction
- Kripke-style models for typed lambda calculus
- Prelogical relations
- GradInf: Gradient Estimation as Probabilistic Inference
- Recognizability, hypergraph operations, and logical types
- The behavior-realization adjunction and generalized homomorphic relations
- An intersection problem for finite automata
- Finitary PCF is not decidable
- Polymorphic rewriting conserves algebraic strong normalization
- Types, abstraction, and parametric polymorphism, part 2
- A semantic characterization of the well-typed formulae of \(\lambda\)- calculus
- A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++
- Relative full completeness for bicategorical Cartesian closed structure
- scientific article; zbMATH DE number 1342281 (Why is no real title available?)
- A fibrational tale of operational logical relations: pure, effectful and differential
- A verified framework for higher-order uncurrying optimizations
- Bialgebraic reasoning on higher-order program equivalence
- Weak consequence relation between -terms
- scientific article; zbMATH DE number 7199581 (Why is no real title available?)
- An algebraic generalization of Frege structures -- binding algebras
- Logical relations for monadic types
- Semantic analysis of normalisation by evaluation for typed lambda calculus
- Intuitive counterexamples for constructive fallacies
- Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
- scientific article; zbMATH DE number 515743 (Why is no real title available?)
- A robust graph-based approach to observational equivalence
- Program equivalence in linear contexts
- Linear Läuchli semantics
- Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels
- Preface
- Unary PCF is decidable
- scientific article; zbMATH DE number 1948186 (Why is no real title available?)
- scientific article; zbMATH DE number 2185710 (Why is no real title available?)
- Fixpoint constructions in focused orthogonality models of linear logic
- An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras
- A generalization of the Takeuti-Gandy interpretation
- scientific article; zbMATH DE number 6744295 (Why is no real title available?)
- Safe recursion with higher types and BCK-algebra
- Selective strictness and parametricity in structural operational semantics, inequationally
- The \(HOL\) logic extended with quantification over type variables
- A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go
- Specification and verification of object-oriented programs using supertype abstraction
- Semantic preservation for a type directed translation scheme of Featherweight Go
- Fully abstract translations between functional languages
- Taming the merge operator
- A note on logical PERs and reducibility. Logical relations strike again!
- scientific article; zbMATH DE number 3878894 (Why is no real title available?)
- A Gentzen-style monadic translation of Gödel's system T
- Linear logical relations and observational equivalences for session-based concurrency
- Logical predicates in higher-order mathematical operational semantics
- scientific article; zbMATH DE number 851066 (Why is no real title available?)
- Syntactic logical relations for polymorphic and recursive types
- Relational interpretations of recursive types in an operational setting.
- Mechanizing logical relations
- Some logical and syntactical observations concerning the first-order dependent type system λP
- Relational and Kleene-Algebraic Methods in Computer Science
- On abstraction and the expressive power of programming languages
- Constructive set theoretic models of typed combinatory logic
- Call-by-value and call-by-name: a simple proof of a classic theorem
- Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them
- Toward a geometry for syntax
- Reducibility: a ubiquitous method in lambda calculus with intersection types
- scientific article; zbMATH DE number 4014020 (Why is no real title available?)
- Behavioural inverse limit -models
- Term-generic logic
- Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations
- A lambda proof of the P-W theorem
- scientific article; zbMATH DE number 3933030 (Why is no real title available?)
- A characterization of lambda definability in categorical models of implicit polymorphism
- Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves
- Semantics of a relational \(\lambda\)-calculus
This page was built for publication: Logical relations and the typed λ-calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3724297)
