LCF considered as a programming language
From MaRDI portal
Publication:1243117
DOI10.1016/0304-3975(77)90044-5zbMath0369.68006DBLPjournals/tcs/Plotkin77OpenAlexW2007270285WikidataQ29395195 ScholiaQ29395195MaRDI QIDQ1243117
Publication date: 1978
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(77)90044-5
Related Items (only showing first 100 items - show all)
A stream calculus of bottomed sequences for real number computation ⋮ Infinitary lambda calculus and discrimination of Berarducci trees. ⋮ Structured algebraic specifications: A kernel language ⋮ A theory for nondeterminism, parallelism, communication, and concurrency ⋮ The origins of structural operational semantics ⋮ From IF to BI. A tale of dependence and separation ⋮ An approach to deciding the observational equivalence of Algol-like languages ⋮ Toward formal development of programs from algebraic specifications: Implementations revisited ⋮ Computational adequacy of the FIX-logic ⋮ PCF extended with real numbers ⋮ Call-by-push-value: Decomposing call-by-value and call-by-name ⋮ Semantics vs syntax vs computations: Machine models for type-2 polynomial-time bounded functionals ⋮ Full abstraction for the second order subset of an Algol-like language ⋮ On the Jacopini technique ⋮ Full abstraction and limiting completeness in equational languages ⋮ On the relations between monadic semantics ⋮ \(\mathbb{T}^\omega\) as a universal domain ⋮ Intuitionistic completeness of first-order logic ⋮ Abstraction for concurrent objects ⋮ A general adequacy result for a linear functional language ⋮ Degrees of parallelism in the continuous type hierarchy ⋮ A relational semantics for parallelism and non-determinism in a functional setting ⋮ Term rewriting for normalization by evaluation. ⋮ The Scott model of linear logic is the extensional collapse of its relational model ⋮ A synthetic axiomatization of map theory ⋮ A mathematical semantics for a nondeterministic typed lambda-calculus ⋮ The IO- and OI-hierarchies ⋮ Domain interpretations of Martin-Löf's partial type theory ⋮ Constructive Boolean circuits and the exactness of timed ternary simulation ⋮ Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation ⋮ Sequential algorithms on concrete data structures ⋮ Domain theory in logical form ⋮ Krivine machines and higher-order schemes ⋮ Correctness of concurrent processes ⋮ About primitive recursive algorithms ⋮ Full abstraction for non-deterministic and probabilistic extensions of PCF. I: The angelic cases ⋮ Relation algebraic domain constructions ⋮ On the expressive power of finitely typed and universally polymorphic recursive procedures ⋮ Semantics for data parallel computation ⋮ Filter models for conjunctive-disjunctive \(\lambda\)-calculi ⋮ Fully abstract compositional semantics for an algebra of logic programs ⋮ New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic ⋮ Characterizing complexity classes by higher type primitive recursive definitions ⋮ Towards a theory of parallel algorithms on concrete data structures ⋮ Fully abstract trace semantics for protected module architectures ⋮ Confluence of the lambda calculus with left-linear algebraic rewriting ⋮ A uniform treatment of order of evaluation and aggregate update ⋮ On stable domains ⋮ An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus ⋮ A domain model characterising strong normalisation ⋮ Subrecursive hierarchies on Scott domains ⋮ Partial inductive definitions as type-systems for \(\lambda\)-terms ⋮ Total sets and objects in domain theory ⋮ Probabilistic coherence spaces as a model of higher-order probabilistic computation ⋮ The equational theory of prebisimilarity over basic CCS with divergence ⋮ A fully abstract may testing semantics for concurrent objects ⋮ Completeness results for the equivalence of recursive schemas ⋮ Fully abstract models of typed \(\lambda\)-calculi ⋮ Operational domain theory and topology of sequential programming languages ⋮ Abstract interface behavior of object-oriented languages with monitors ⋮ A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++ ⋮ A syntactic theory of sequential state ⋮ The semantics of second-order lambda calculus ⋮ Functorial polymorphism ⋮ Applications of infinitary lambda calculus ⋮ Natural non-dcpo domains and f-spaces ⋮ A unary representation result for system \(T\) ⋮ Induction and recursion on the partial real line with applications to Real PCF ⋮ Semantics of algorithmic languages ⋮ System \(T\), call-by-value and the minimum problem ⋮ Unary PCF is decidable ⋮ Distributive semantics for nondeterministic typed \(\lambda\)-calculi ⋮ Expressive power of typed and type-free programming languages ⋮ Computable de Finetti measures ⋮ The extensional ordering of the sequential functionals ⋮ Describing semantic domains with sprouts ⋮ Two-level languages for program optimization ⋮ Decidability of behavioural equivalence in unary PCF ⋮ On the semantics of polymorphism ⋮ Properly injective spaces and function spaces ⋮ From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models ⋮ The sequentially realizable functionals ⋮ \({\mathcal M}^\omega\) considered as a programming language ⋮ A relative PCF-definability result for strongly stable functions and some corollaries ⋮ Relational interpretations of recursive types in an operational setting. ⋮ Games and full abstraction for FPC. ⋮ Integration in Real PCF ⋮ Full abstraction for PCF ⋮ Encoding linear logic with interaction combinators ⋮ On inner classes ⋮ Ordered SOS process languages for branching and eager bisimulations ⋮ Nonexpressibility of fairness and signaling ⋮ Computational foundations of basic recursive function theory ⋮ General recursive functions in a very simply interpretable typed \(\lambda\)-calculus ⋮ Historical introduction to ``Concrete domains by G. Kahn and G. D. Plotkin ⋮ Combinatory reduction systems: Introduction and survey ⋮ A type-theoretical alternative to ISWIM, CUCH, OWHY ⋮ Relative definability of boolean functions via hypergraphs ⋮ Exact real number computations relative to hereditarily total functionals. ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
Uses Software
Cites Work
This page was built for publication: LCF considered as a programming language