Full abstraction in the lazy lambda calculus
From MaRDI portal
Publication:1261291
DOI10.1006/inco.1993.1044zbMath0779.03003OpenAlexW2088941870WikidataQ56443859 ScholiaQ56443859MaRDI QIDQ1261291
Publication date: 1 September 1993
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/inco.1993.1044
Stone dualityfilter modeldenotational semanticsdomain logicinitial solution of domain equationlazy \(\lambda\)- modelslazy call-by-name \(\lambda\)-calculus
Semantics in the theory of computing (68Q55) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)
Related Items
Infinitary lambda calculus and discrimination of Berarducci trees. ⋮ Proving soundness of extensional normal-form bisimilarities ⋮ A categorical framework for congruence of applicative bisimilarity in higher-order languages ⋮ Intersection types and lambda models ⋮ Games characterizing Levy-Longo trees ⋮ Adapting innocent game models for the Böhm tree \(\lambda\)-theory ⋮ Parametric parameter passing \(\lambda\)-calculus ⋮ On Applicative Similarity, Sequentiality, and Full Abstraction ⋮ Infinitary lambda calculi and böhm models ⋮ A logical approach to stable domains ⋮ A class of bounded functions, a database language and an extended lambda calculus ⋮ Labelled reductions, runtime errors, and operational subsumption ⋮ A lambda-calculus for dynamic binding ⋮ Fairness and communication-based semantics for session-typed languages ⋮ Highlights in infinitary rewriting and lambda calculus ⋮ A first order logic of effects ⋮ Infinitary lambda calculus ⋮ From semantics to types: the case of the imperative \(\lambda\)-calculus ⋮ Algebraic interpretation of lambda calculus with resources ⋮ Program equivalence in an untyped, call-by-value functional language with uncurried functions ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ The untyped computational \(\lambda \)-calculus and its intersection type discipline ⋮ Parametric \(\lambda \)-theories ⋮ An irregular filter model ⋮ Behavioural inverse limit \(\lambda\)-models ⋮ Domain theory for concurrency ⋮ Filter models for conjunctive-disjunctive \(\lambda\)-calculi ⋮ A bisimulation for dynamic sealing ⋮ A calculus of mobile processes. I ⋮ From Böhm's Theorem to Observational Equivalences ⋮ Towards Lambda Calculus Order-Incompleteness ⋮ Logical equivalence for subtyping object and recursive types ⋮ Strong normalization from an unusual point of view ⋮ Unfixing the Fixpoint: The Theories of the λY-Calculus ⋮ On the observational theory of the CPS-calculus ⋮ Intersection Types and Computational Rules ⋮ Game semantics and linear CPS interpretation ⋮ A fully abstract may testing semantics for concurrent objects ⋮ Coalgebraic description of generalised binary methods ⋮ Intersection types for \(\lambda\)-trees ⋮ From rewrite rules to bisimulation congruences ⋮ Recursive Domain Equations of Filter Models ⋮ Call-by-value Solvability ⋮ Lazy Lambda calculus: Theories, models and local structure characterization ⋮ Proof, meaning and paradox: some remarks ⋮ RPO, Second-Order Contexts, and λ-Calculus ⋮ Logical Semantics for Stability ⋮ Unnamed Item ⋮ Applications of infinitary lambda calculus ⋮ A Fresh Look at the λ-Calculus ⋮ Infinite \(\lambda\)-calculus and types ⋮ Semantical analysis of perpetual strategies in \(\lambda\)-calculus ⋮ Small-step and big-step semantics for call-by-need ⋮ Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types. ⋮ Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic ⋮ A Fully Abstract Model for Mobile Ambients ⋮ Simple Easy Terms ⋮ Compositional characterisations of \(\lambda\)-terms using intersection types ⋮ From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models ⋮ Observational program calculi and the correctness of translations ⋮ Discrimination by parallel observers: the algorithm. ⋮ Descendants and origins in term rewriting. ⋮ An abstract framework for environment machines ⋮ A co-induction principle for recursively defined domains ⋮ A fully abstract denotational semantics for the \(\pi\)-calculus ⋮ The infinitary lambda calculus of the infinite eta Böhm trees ⋮ Clocked lambda calculus ⋮ Full abstraction for lambda calculus with resources and convergence testing
Uses Software
