Call-by-name, call-by-value and the \(\lambda\)-calculus

DOI10.1016/0304-3975(75)90017-1zbMath0325.68006WikidataQ29041781 ScholiaQ29041781MaRDI QIDQ1225449

Publication date: 1975

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

Full work available at URL: https://doi.org/10.1016/0304-3975(75)90017-1

Mathematics Subject Classification ID

68N01: General topics in the theory of software

03B40: Combinatory logic and lambda calculus

Related Items

Representing Control: a Study of the CPS Transformation, From operational semantics to abstract machines, Comprehending monads, Fully abstract translations between functional languages, The Impact of the Lambda Calculus in Logic and Computer Science, Unnamed Item, A new deconstructive logic: linear logic, Proofs of strong normalisation for second order classical natural deduction, Representing Control: a Study of the CPS Transformation, Unnamed Item, Strong normalization proof with CPS-translation for second order classical natural deduction, A categorical understanding of environment machines, Proving the correctness of compiler optimisations based on a global analysis: a study of strictness analysis^†, Sound and complete axiomatisations of call-by-value control operators, Reference counting as a computational interpretation of linear logic, Formal basis for the refinement of rule based transition systems, A partial evaluator for the untyped lambda-calculus, Equivalence in functional languages with effects, Call-by-value Solvability, On one-pass CPS transformations, On categorical models of classical logic and the Geometry of Interaction, Operational interpretations of an extension of F_ω with control operators, On the semantics of classical disjunction, Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models, Weak normalization implies strong normalization in a class of non-dependent pure type systems, An induction principle for pure type systems, Proving the correctness of recursion-based automatic program transformations, Computational interpretations of linear logic, Using typed lambda calculus to implement formal systems on a machine, Notions of computation and monads, An abstract framework for environment machines, Comparison of priority rules in pattern matching and term rewriting, Call-by-push-value: Decomposing call-by-value and call-by-name, Combining algebraic effects with continuations, A syntactic correspondence between context-sensitive calculi and abstract machines, A short proof of the lexical addressing algorithm, Parametric \(\lambda \)-theories, Types as graphs: Continuations in type logical grammar, A syntactic theory of sequential control, Decidability of the restriction equational theory in the partial lambda calculus, A mathematical semantics for a nondeterministic typed lambda-calculus, Inferring the equivalence of functional programs that mutate data, The revised report on the syntactic theories of sequential control and state, A theory for program and data type specification, LCF considered as a programming language, A syntactic theory of sequential state, Semantical analysis of perpetual strategies in \(\lambda\)-calculus, A behavioural theory of first-order CML, Synthesis of ML programs in the system Coq, Classical logic, storage operators and second-order lambda-calculus, A general storage theorem for integers in call-by-name \(\lambda\)- calculus, A constructive logic behind the catch and throw mechanism, Computational adequacy of the FIX-logic, A meta-language for typed object-oriented languages, Strong normalization from weak normalization in typed \(\lambda\)-calculi, A first order logic of effects, A general adequacy result for a linear functional language, A confluent calculus for concurrent constraint programming, On the strong normalisation of intuitionistic natural deduction with permutation-conversions, On the semantics of the call-by-name CPS transform, Actor languages. Their syntax, semantics, translation, and equivalence, From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models, Game semantics and linear CPS interpretation, Axioms for strict and lazy functional programs, About classical logic and imperative programming, An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus., Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus, Relational interpretations of recursive types in an operational setting., Perpetuality and uniform normalization in orthogonal rewrite systems, Assigning types to processes, Conservation and uniform normalization in lambda calculi with erasing reductions, The origins of structural operational semantics, Games characterizing Levy-Longo trees, A first-order one-pass CPS transformation, Parametric parameter passing \(\lambda\)-calculus, On the call-by-value CPS transform and its semantics, Variations on mobile processes, Game-theoretic analysis of call-by-value computation, Intersection types and lambda models, State-transition machines for lambda-calculus expressions, Axioms for control operators in the CPS hierarchy, A static simulation of dynamic delimited control, On the unity of duality, Completeness of continuation models for \(\lambda_\mu\)-calculus, A functional correspondence between monadic evaluators and abstract machines for languages with computational effects, Order-enriched categorical models of the classical sequent calculus, A structural approach to reversible computation, Domain-Freeλµ-Calculus, European Summer Meeting of the Association for Symbolic Logic, Hull, 1986, Mechanized Verification of CPS Transformations, Safety of Nöcker's strictness analysis, A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case, Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence, Meeting of the Association for Symbolic Logic, Stanford, California, 1985, Unnamed Item, Functions as processes

Uses Software

ALGOL 60

Cites Work