LCF considered as a programming language
From MaRDI portal
Publication:1243117
DOI10.1016/0304-3975(77)90044-5zbMath0369.68006OpenAlexW2007270285WikidataQ29395195 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
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, Equationally fully abstract models of PCF, Termination, deadlock and divergence, Computational adequacy via ‘mixed’ inductive definitions, An investigation into functions as processes, Sequential functions on indexed domains and full abstraction for a sub-language of PCF, Another approach to sequentiality: Kleene's unimonotone functions, Mechanizing logical relations, Constructive set theoretic models of typed combinatory logic, Denotational aspects of untyped normalization by evaluation, Program equivalence in a typed probabilistic call-by-need functional language, Streams of approximations, equivalence of recursive effectful programs, From operational to denotational semantics, Simultaneous substitution in the typed lambda calculus, Continuous functions and parallel algorithms on concrete data structures, A pragmatic approach to stateful partial order reduction, A coherent differential PCF, Apartness, sharp elements, and the Scott topology of domains, Parallelism in realizability models, Correctness of compiling polymorphism to dynamic typing, No value restriction is needed for algebraic effects and handlers, Unnamed Item, A model of PCF in guarded type theory, Clocks for Functional Programs, An operational domain-theoretic treatment of recursive types, Full abstraction for expressiveness: history, myths and facts, On the ubiquity of certain total type structures, Strictness, totality, and non-standard-type inference, Two applications of analytic functors, On the construction of stable models of untyped \(\lambda\)-calculus, A typed context calculus, Finitary PCF is not decidable, On the expressive power of first-order boolean functions in PCF, From Logic to Theoretical Computer Science – An Update, On Natural Non-dcpo Domains, Computing with Functionals—Computability Theory or Computer Science?, Denotational Semantics with Nominal Scott Domains, Redexes are stable in the λ-calculus, Clocked lambda calculus, Computing in unpredictable environments: Semantics, reduction strategies, and program transformations, Behavioural satisfaction and equivalence in concrete model categories, Untyped lambda-calculus with input-output, Characteristic bisimulation for higher-order session processes, 1998 European Summer Meeting of the Association for Symbolic Logic, Taylor expansion, finiteness and strategies, Quantitative logics for equivalence of effectful programs, Computational adequacy for recursive types in models of intuitionistic set theory, Continuous probability distributions in concurrent games, On Applicative Similarity, Sequentiality, and Full Abstraction, Semantics of a sequential language for exact real-number computation, The Scott model of PCF in univalent type theory, Probabilistic operational semantics for the lambda calculus, Interdefinability of parallel operations in PCF, Towards the computational complexity of \(\mathcal{PR}^ \omega\)-terms, Recursive programs and denotational semantics in absolute logics of programs, A domain equation for bisimulation, Fully abstract translations between functional languages, A universality theorem for PCF with recursive types, parallel-or and ∃, A two-level logic approach to reasoning about computations, Game semantics approach to higher-order complexity, Constructive natural deduction and its ‘ω-set’ interpretation, Game theoretic analysis of call-by-value computation, Games and full completeness for multiplicative linear logic, Projecting sequential algorithms on strongly stable functions, Size-based termination of higher-order rewriting, Full abstraction and the Context Lemma (preliminary report), Stable bistructure models of PCF, Full abstraction for the second order subset of an ALGOL-like language, N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker, Categorical semantics of a simple differential programming language, A Denotational Semantics for Total Correctness of Sequential Exact Real Programs, On naturally continuous non-dcpo domains, Latent semantic analysis of game models using LSTM, Interpreting Localized Computational Effects Using Operators of Higher Type, Normal forms, linearity, and prime algebraicity over nonflat domains, Continuity in Semantic Theories of Programming, Simply typed fixpoint calculus and collapsible pushdown automata, Block structure vs scope extrusion: between innocence and omniscience, Unnamed Item, Sequential real number computation and recursive relations, An abstract data type for real numbers, Game-theoretic analysis of call-by-value computation, Note on Algol and conservatively extending functional programming, Intuitionistic fixed point logic, Observed Communication Semantics for Classical Processes, Metric Reasoning About $$\lambda $$-Terms: The General Case, $$\mathsf {qPCF}$$ : A Language for Quantum Circuit Computations, Unnamed Item, A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic, Higher-order processes and their models, A Type Theory for Probabilistic $$\lambda $$–calculus, Reference counting as a computational interpretation of linear logic, Unnamed Item, Unnamed Item, Games and Definability For FPC, Krivine Machines and Higher-Order Schemes, Full abstraction for polymorphic \(\pi \)-calculus, Domains for Computation in Mathematics, Physics and Exact Real Arithmetic, A typed, algebraic, computational lambda-calculus, Sequential Real Number Computation and Recursive Relations, First-Order Universality for Real Programs, Recursive Functions with Pattern Matching in Interaction Nets, Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion, European Summer Meeting of the Association for Symbolic Logic, Hull, 1986, A stable programming language, Introduction to Type Theory, Dependent Types at Work, A Relational Model of a Parallel and Non-deterministic λ-Calculus, Semantical proofs of correctness for programs performing non-deterministic tests on real numbers, A relational account of call-by-value sequentiality, Unnamed Item, On the Cantor–Bendixson rank of a set that is searchable in Gödel’s T, Some Programming Languages Suggested by Game Models (Extended Abstract), Semi-decidability of May, Must and Probabilistic Testing in a Higher-type Setting, Exploratory Functions on Nondeterministic Strategies, up to Lower Bisimilarity, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, A Fully Abstract Semantics for Constructor Systems, A Process-Model for Linear Programs, The Dedekind reals in abstract Stone duality, Unnamed Item, Effective λ-models versus recursively enumerable λ-theories, Full Abstraction at Package Boundaries of Object-Oriented Languages, Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages, On abstraction and the expressive power of programming languages, Dynamic game semantics, A game-semantic model of computation, Unnamed Item, Unnamed Item, An implementation model of the typed λ-calculus based on Linear Chemical Abstract Machine, On a monadic semantics for freshness, QPCF: higher-order languages and quantum circuits, Sequential algorithms and strongly stable functions, An abstract data type for real numbers, Observational program calculi and the correctness of translations, Logical Relations and Nondeterminism, Aspects of Categorical Recursion Theory, Syntactic Logical Relations for Polymorphic and Recursive Types, Definability and Full Abstraction, Program equivalence in linear contexts
Uses Software
Cites Work
