Full abstraction for PCF

DOI10.1006/inco.2000.2930zbMath1006.68028DBLPjournals/iandc/AbramskyJM00OpenAlexW2165446401WikidataQ56443857 ScholiaQ56443857MaRDI QIDQ1854394

Radha Jagadeesan, Samson Abramsky, Pasquale Malacaria

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: http://qmro.qmul.ac.uk/xmlui/handle/123456789/13604

zbMATH Keywords

definability PCF recursive strategy fully abstract model intensional model

Mathematics Subject Classification ID

Applications of game theory (91A80) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Categorical semantics of formal languages (18C50) Recursive functions and relations, subrecursive hierarchies (03D20) Combinatory logic and lambda calculus (03B40) Enriched categories (over closed or monoidal categories) (18D20)

Related Items (only showing first 100 items - show all)

Non-linearity as the Metric Completion of Linearity ⋮ The geometry of Bayesian programming ⋮ Smart Choices and the Selection Monad ⋮ Arboreal Categories: An Axiomatic Theory of Resources ⋮ Game semantics of Martin-Löf type theory ⋮ Unnamed Item ⋮ Logic and Geometry of Agents in Agent-Based Modeling ⋮ On the reification of semantic linearity ⋮ A fully abstract denotational semantics for the calculus of higher-order communicating systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On Natural Non-dcpo Domains ⋮ On-the-Fly Techniques for Game-Based Software Model Checking ⋮ A Theory for Game Theories ⋮ Unnamed Item ⋮ Epistemic Strategies and Games on Concurrent Processes ⋮ Unnamed Item ⋮ Denotational Semantics with Nominal Scott Domains ⋮ Type-Based Security for Mobile Computing Integrity, Secrecy and Liveness ⋮ Infinitary affine proofs ⋮ Redexes are stable in the λ-calculus ⋮ Characteristic bisimulation for higher-order session processes ⋮ On concurrent games with payoff ⋮ The category of node-and-choice preforms for extensive-form games ⋮ Computation by interaction for space-bounded functional programming ⋮ A Semantical Approach to Equilibria and Rationality ⋮ Constructive Game Logic ⋮ Games characterizing Levy-Longo trees ⋮ Adapting innocent game models for the Böhm tree $\lambda$-theory ⋮ Polarized games ⋮ An approach to deciding the observational equivalence of Algol-like languages ⋮ Continuous probability distributions in concurrent games ⋮ Games for Dependent Types ⋮ Parsimonious Types and Non-uniform Computation ⋮ Understanding Game Semantics Through Coherence Spaces ⋮ Geometry of Synthesis II: From Games to Delay-Insensitive Circuits ⋮ Game Semantics in the Nominal Model ⋮ A System-Level Game Semantics ⋮ A Graphical Foundation for Schedules ⋮ Game semantics for dependent types ⋮ Types and full abstraction for polyadic $\pi$-calculus ⋮ From Coalgebraic to Monoidal Traces ⋮ Semantics of higher-order quantum computation via geometry of interaction ⋮ Strong normalisation in the $\pi$-calculus ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Imperative programs as proofs via game semantics ⋮ Full abstraction for Reduced ML ⋮ A game semantics for disjunctive logic programming ⋮ Verifying annotated program families using symbolic game semantics ⋮ Multigames and strategies, coalgebraically ⋮ On naturally continuous non-dcpo domains ⋮ Glueing and orthogonality for models of linear logic ⋮ Latent semantic analysis of game models using LSTM ⋮ Deterministic concurrent strategies ⋮ Constructive semantics for instantaneous reactions ⋮ A curry-style semantics of interaction: from untyped to second-order lazy $\lambda\mu$-calculus ⋮ Resource modalities in tensor logic ⋮ Proof and refutation in MALL as a game ⋮ Mackey-complete spaces and power series – a topological model of differential linear logic ⋮ The relational model is injective for multiplicative exponential linear logic (without weakenings) ⋮ Curry-style type isomorphisms and game semantics ⋮ Block structure vs scope extrusion: between innocence and omniscience ⋮ Program equivalence in a simple language with state ⋮ Weighted models for higher-order computation ⋮ A Truly Concurrent Game Model of the Asynchronous $$\pi $$-Calculus ⋮ ML and Extended Branching VASS ⋮ A type assignment system for game semantics ⋮ Full abstraction for non-deterministic and probabilistic extensions of PCF. I: The angelic cases ⋮ A graphical foundation for interleaving in game semantics ⋮ The Category of Node-and-Choice Forms, with Subcategories for Choice-Sequence Forms and Choice-Set Forms ⋮ Complete trace models of state and control ⋮ Bayesian strategies: probabilistic programs as generalised graphical models ⋮ Symmetry and Interactivity in Programming ⋮ Algorithmic probabilistic game semantics. Playing games with automata ⋮ Second-order type isomorphisms through game semantics ⋮ A game semantics of names and pointers ⋮ Preface to the special volume ⋮ Musings around the geometry of interaction, and coherence ⋮ Payoffs, Intensionality and Abstraction in Games ⋮ Unfixing the Fixpoint: The Theories of the λY-Calculus ⋮ Towards Nominal Abramsky ⋮ Unnamed Item ⋮ An exact correspondence between a typed pi-calculus and polarised proof-nets ⋮ Game semantics and linear CPS interpretation ⋮ A stable programming language ⋮ Linear realizability and full completeness for typed lambda-calculi ⋮ A fully abstract may testing semantics for concurrent objects ⋮ A game semantics for generic polymorphism ⋮ Asynchronous games. II: The true concurrency of innocence ⋮ Linearity and bisimulation ⋮ Least and Greatest Fixpoints in Game Semantics ⋮ Full Abstraction for Reduced ML ⋮ Compositional Predicate Abstraction from Game Semantics ⋮ Toward the interpretation of non-constructive reasoning as non-monotonic learning ⋮ Game Semantics for Access Control ⋮ Unnamed Item ⋮ Operational domain theory and topology of sequential programming languages ⋮ Partial Orders, Event Structures and Linear Strategies

Cites Work

This page was built for publication: Full abstraction for PCF