Fully abstract models of typed $\lambda$-calculi

DOI10.1016/0304-3975(77)90053-6zbMath0386.03006OpenAlexW2039112578WikidataQ29012844 ScholiaQ29012844MaRDI QIDQ1249567

Publication date: 1977

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/15112912/1_s2.0_0304397577900536_main.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items

Equationally fully abstract models of PCF, Generalization of final algebra semantics by relativization, Termination, deadlock and divergence, An investigation into functions as processes, Sequential functions on indexed domains and full abstraction for a sub-language of PCF, Streams of approximations, equivalence of recursive effectful programs, From operational to denotational semantics, Continuous functions and parallel algorithms on concrete data structures, On the ubiquity of certain total type structures, Minimality and separation results on asynchronous mobile processes -- representability theorems by concurrent combinators, A typed context calculus, Finitary PCF is not decidable, On the expressive power of first-order boolean functions in PCF, On Natural Non-dcpo Domains, Computing with Functionals—Computability Theory or Computer Science?, Behavioural satisfaction and equivalence in concrete model categories, Untyped lambda-calculus with input-output, Characteristic bisimulation for higher-order session processes, Infinitary lambda calculus and discrimination of Berarducci trees., Structured algebraic specifications: A kernel language, About fair asynchrony, From IF to BI. A tale of dependence and separation, Stability, sequentiality and demand driven evaluation in dataflow, Fully abstract submodels of typed lambda calculi, Applicative Bisimulation and Quantum λ-Calculi, On reduction-based process semantics, Parameter-reduction of higher level grammars, A domain equation for bisimulation, Types and full abstraction for polyadic $\pi$-calculus, Fully abstract translations between functional languages, Partial ordering models for concurrency can be defined operationally, Full abstraction for the second order subset of an Algol-like language, Game theoretic analysis of call-by-value computation, Full abstraction and limiting completeness in equational languages, Linear Läuchli semantics, Projecting sequential algorithms on strongly stable functions, Functions as processes, Full abstraction and the Context Lemma (preliminary report), Fairness and communication-based semantics for session-typed languages, Stable bistructure models of PCF, A first order logic of effects, (Modular) Effect Algebras are Equivalent to (Frobenius) Antispecial Algebras, Proof systems for structured specifications with observability operators, Normal forms, linearity, and prime algebraicity over nonflat domains, A trace-based service semantics guaranteeing deadlock freedom, Continuity in Semantic Theories of Programming, A mathematical semantics for a nondeterministic typed lambda-calculus, Reasoning about multi-stage programs, Unnamed Item, Note on Algol and conservatively extending functional programming, Partial abstract types, Sequential algorithms on concrete data structures, Modular Verification of Procedure Equivalence in the Presence of Memory Allocation, Unnamed Item, Unnamed Item, Domain theory in logical form, Unnamed Item, Correctness of concurrent processes, Full abstraction for non-deterministic and probabilistic extensions of PCF. I: The angelic cases, Towards a semantics-based information theory, Unnamed Item, Complete trace models of state and control, Unnamed Item, Observational interpretations of hybrid dynamic logic with binders and silent transitions, Algorithm design through the optimization of reuse-based generation, Behavioural theories and the proof of behavioural properties, Fully abstract compositional semantics for an algebra of logic programs, Towards a theory of parallel algorithms on concrete data structures, Fully abstract trace semantics for protected module architectures, Symmetry and Interactivity in Programming, Full abstraction for polymorphic $\pi $-calculus, Algorithmic probabilistic game semantics. Playing games with automata, Modal logic and algebraic specifications, On stable domains, On generic context lemmas for higher-order calculi with sharing, Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi, European Summer Meeting of the Association for Symbolic Logic, Hull, 1986, Principal types of BCK-lambda-terms, Unnamed Item, On the observational theory of the CPS-calculus, The equational theory of prebisimilarity over basic CCS with divergence, A stable programming language, A fully abstract may testing semantics for concurrent objects, Axioms for strict and lazy functional programs, Asynchronous games. II: The true concurrency of innocence, A relational account of call-by-value sequentiality, Formal Analysis of Dynamic, Distributed File-System Access Controls, Unnamed Item, The typed lambda-calculus is not elementary recursive, Operational domain theory and topology of sequential programming languages, Abstract interface behavior of object-oriented languages with monitors, Unnamed Item, Unnamed Item, The semantics of second-order lambda calculus, Can LCF be topped! Flat lattice models of typed $\lambda{}$-calculus, On an effective hierarchy of communicating processes: Separation principle and testing, Natural non-dcpo domains and f-spaces, Distributive semantics for nondeterministic typed $\lambda$-calculi, Full Abstraction at Package Boundaries of Object-Oriented Languages, Expressive power of typed and type-free programming languages, On abstraction and the expressive power of programming languages, The extensional ordering of the sequential functionals, Une critique de la notion de test de processus fondée sur la non séparabilité de certaines classes de langages, A case study in programming coinductive proofs: Howe’s method, The sequential functionals of type $(\iota \rightarrow \iota)^n \rightarrow \iota$ form a dcpo for all $n \in \Bbb N$, Decidability of behavioural equivalence in unary PCF, Processes against tests: on defining contextual equivalences, The insensitivity theorem for nonreducing reflexive types, The sequentially realizable functionals, Observational program calculi and the correctness of translations, A relative PCF-definability result for strongly stable functions and some corollaries, Games and full abstraction for FPC., Full abstraction for PCF, Definability and Full Abstraction, A systematic study of models of abstract data types, Sequentiality and the CPS Semantics of Fresh Names, Historical introduction to ``Concrete domains by G. Kahn and G. D. Plotkin

Cites Work

Fully abstract models of typed \(\lambda\)-calculi