Proving congruence of bisimulation in functional programming languages
From MaRDI portal
Publication:1917068
DOI10.1006/inco.1996.0008zbMath0853.68073OpenAlexW2092367588MaRDI QIDQ1917068
Publication date: 3 July 1996
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/20c81467bbfc707169c5aac3e064e8f43e9de5b9
Related Items
Applicative bisimilarities for call-by-name and call-by-value \(\lambda\mu\)-calculus, A categorical framework for congruence of applicative bisimilarity in higher-order languages, A format for semantic equivalence comparison, On bisimilarity in lambda calculi with continuous probabilistic choice, Quantitative logics for equivalence of effectful programs, Applicative Bisimulation and Quantum λ-Calculi, Howe’s Method for Calculi with Passivation, A Complete, Co-inductive Syntactic Theory of Sequential Control and State, Encoding abstract syntax without fresh names, A two-valued logic for properties of strict functional programs allowing partial functions, SOS formats and meta-theory: 20 years after, Fairness and communication-based semantics for session-typed languages, On Equivalences, Metrics, and Polynomial Time, Complete Lattices and Up-To Techniques, Operational equivalence for interaction nets., On the expressiveness and decidability of higher-order process calculi, 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, A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case, Reasoning about multi-stage programs, Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report), Characterizing contextual equivalence in calculi with passivation, Unnamed Item, A bisimulation for dynamic sealing, Effectful applicative similarity for call-by-name lambda calculi, Process calculus based upon evaluation to committed form, On generic context lemmas for higher-order calculi with sharing, Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi, Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion, Variable binding operators in transition system specifications, From Applicative to Environmental Bisimulation, On the representation of McCarthy's \(amb\) in the \(\pi\)-calculus, An operational domain-theoretic treatment of recursive types, Axioms for strict and lazy functional programs, \(\mathrm{HO}\pi\) in Coq, Normal Bisimulations in Calculi with Passivation, Exploratory Functions on Nondeterministic Strategies, up to Lower Bisimilarity, Unnamed Item, A conservative look at operational semantics with variable binding, Semantical analysis of perpetual strategies in \(\lambda\)-calculus, Process calculus based upon evaluation to committed form, A case study in programming coinductive proofs: Howe’s method, Mechanized metatheory revisited, MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK, Asynchronous process calculi: The first- and higher-order paradigms, Observational program calculi and the correctness of translations, Bisimilarity of open terms., Vertical implementation, Syntactic Logical Relations for Polymorphic and Recursive Types, On Well-Foundedness and Expressiveness of Promoted Tyft, Amb Breaks Well-Pointedness, Ground Amb Doesn't, Bisimulation and Co-induction: Some Problems, Program equivalence in linear contexts, Contextual equivalence for inductive definitions with binders in higher order typed functional programming, Untyped lambda-calculus with input-output
