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

DOI10.1016/0304-3975(75)90017-1zbMath0325.68006OpenAlexW2088735483WikidataQ29041781 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

General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items

Modelling and analysing neural networks using a hybrid process algebra, Classical logic, storage operators and second-order lambda-calculus, Eager functions as processes, A general storage theorem for integers in call-by-name $\lambda$- calculus, The origins of structural operational semantics, A constructive logic behind the catch and throw mechanism, Intersection types and lambda models, 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, Plotkin's call-by-value $\lambda$-calculus as a modal calculus, Strong normalization proofs by CPS-translations, Computational adequacy of the FIX-logic, A meta-language for typed object-oriented languages, Compilation of extended recursion in call-by-value functional languages, Peter J. Landin (1930--2009), A syntactic theory of sequential control, Strong normalization from weak normalization in typed $\lambda$-calculi, Parametric Church's thesis: synthetic computability without choice, Call-by-push-value: Decomposing call-by-value and call-by-name, A functional correspondence between call-by-need evaluators and lazy abstract machines, A two-level logic approach to reasoning about computations, Semantics of higher-order quantum computation via geometry of interaction, A two-valued logic for properties of strict functional programs allowing partial functions, On the value of variables, Decidability of the restriction equational theory in the partial lambda calculus, Combining algebraic effects with continuations, A syntactic correspondence between context-sensitive calculi and abstract machines, Continuation-passing C, compiling threads to events through continuations, A first order logic of effects, A general adequacy result for a linear functional language, A confluent calculus for concurrent constraint programming, A refined interpretation of intuitionistic logic by means of atomic polymorphism, Theory of interaction, Latent semantic analysis of game models using LSTM, On the strong normalisation of intuitionistic natural deduction with permutation-conversions, Proof nets and the call-by-value $\lambda$-calculus, The locally nameless representation, Contextual equivalence for signal flow graphs, A mathematical semantics for a nondeterministic typed lambda-calculus, Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control, The untyped computational $\lambda $-calculus and its intersection type discipline, Delimited control operators prove double-negation shift, A short proof of the lexical addressing algorithm, Variations on mobile processes, Game-theoretic analysis of call-by-value computation, Refunctionalization at work, Type checking and typability in domain-free lambda calculi, Parametric $\lambda $-theories, Intensional computation with higher-order functions, Factorization in call-by-name and call-by-value calculi via linear logic, The spirit of node replication, Proving the correctness of recursion-based automatic program transformations, A formalized general theory of syntax with bindings: extended version, Classical realizability in the CPS target language, Programs as data structures in $\lambda$SF-calculus, Transparent quantification into hyperintensional objectual attitudes, Inferring the equivalence of functional programs that mutate data, The spirit of ghost code, Computational interpretations of linear logic, The revised report on the syntactic theories of sequential control and state, A theory for program and data type specification, Using typed lambda calculus to implement formal systems on a machine, On graph rewriting, reduction, and evaluation in the presence of cycles, On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion, Hypothetical logic of proofs, Strong normalization from an unusual point of view, On the observational theory of the CPS-calculus, On typing delimited continuations: Three new solutions to the printf problem, Evaluating lambda terms with traversals, Game semantics and linear CPS interpretation, Axioms for strict and lazy functional programs, Machine learning guidance for connection tableaux, LCF considered as a programming language, Pedagogical second-order $\lambda $-calculus, Abstracting models of strong normalization for classical calculi, Types as graphs: Continuations in type logical grammar, A syntactic theory of sequential state, About classical logic and imperative programming, Notions of computation and monads, Semantical analysis of perpetual strategies in $\lambda$-calculus, Call-by-value lambda calculus as a model of computation in Coq, A behavioural theory of first-order CML, On the semantics of the call-by-name CPS transform, Actor languages. Their syntax, semantics, translation, and equivalence, CPS transformation of beta-redexes, On the dynamic extent of delimited continuations, CPS-translation as adjoint, From computation to foundations via functions and application: The $\lambda$-calculus and its webbed models, Confluence in probabilistic rewriting, 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, An abstract framework for environment machines, Comparison of priority rules in pattern matching and term rewriting, Synthesis of ML programs in the system Coq, LF+ in Coq for "fast and loose" reasoning, A simplifier for untyped lambda expressions, An investigation into functions as processes, A categorical interpretation of Landin's correspondence principle, On the transformation between direct and continuation semantics, Unnamed Item, Automating the functional correspondence between higher-order evaluators and abstract machines, Understanding algebraic effect handlers via delimited control operators, From operational to denotational semantics, Correctness of procedure representations in higher-order assembly language, A strong call-by-need calculus, Separating Sessions Smoothly, Galois connecting call-by-value and call-by-name, Call-by-value combinatory logic and the lambda-value calculus, Node Replication: Theory And Practice, Quantitative global memory, Towards an induction principle for nested data types, Parallelism in realizability models, Reasoning about multi-stage programs, Call-by-name extensionality and confluence, Observing Success in the Pi-Calculus, Head reduction and normalization in a call-by-value lambda-calculus, Structural Rewriting in the pi-Calculus., Operational interpretations of an extension of F_ω with control operators, Monadic translation of classical sequent calculus, A Partial Type Checking Algorithm for Type:Type, On the semantics of classical disjunction, On one-pass CPS transformations, On categorical models of classical logic and the Geometry of Interaction, Introduction to Type Theory, 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, Unnamed Item, Unnamed Item, CONSTRUCTIVE CLASSICAL LOGIC AS CPS-CALCULUS, On reduction and normalization in the computational core, Z property for the shuffling calculus, Relating Functional and Imperative Session Types, A Functional Abstraction of Typed Invocation Contexts, Optimal solutions to pattern matching problems, Unnamed Item, Unnamed Item, From Outermost Reduction Semantics to Abstract Machine, Lazy rewriting and eager machinery, Probabilistic operational semantics for the lambda calculus, On the enumeration of closures and environments with an application to random generation, A Nominal Relational Model for Local Store, Continuation Models for the Lambda Calculus With Constructors, Call-by-Value Non-determinism in a Linear Logic Type Discipline, Open Call-by-Value, Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation, Representing Control: a Study of the CPS Transformation, From operational semantics to abstract machines, Comprehending monads, A Complete, Co-inductive Syntactic Theory of Sequential Control and State, Unnamed Item, Unnamed Item, Unnamed Item, Fully abstract translations between functional languages, Unnamed Item, A proof theoretical approach to communication, A semantics preserving actor translation, Labelled reductions, runtime errors, and operational subsumption, Proofs, Upside Down, Functions as processes, Meeting of the Association for Symbolic Logic, Stanford, California, 1985, Non-speculative and upward invocation of continuations in a parallel language, Extensional Logic of Hyperintensions, Mechanized Verification of CPS Transformations, Unnamed Item, How to prove decidability of equational theories with second-order computation analyser SOL, Effect handlers via generalised continuations, Safety of Nöcker's strictness analysis, Light logics and higher-order processes, A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case, Conversion to tail recursion in term rewriting, Unnamed Item, On the semantics of parsing actions, 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, Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence, The Impact of the Lambda Calculus in Logic and Computer Science, A Type Theory for Probabilistic $$\lambda $$–calculus, Reference counting as a computational interpretation of linear logic, Formal basis for the refinement of rule based transition systems, Unnamed Item, Domain-Freeλµ-Calculus, State-transition machines for lambda-calculus expressions, Axioms for control operators in the CPS hierarchy, A static simulation of dynamic delimited control, Classical Call-by-Need and Duality, A new deconstructive logic: linear logic, Covert Movement in Logical Grammar, Strong normalization proof with CPS-translation for second order classical natural deduction, Proofs of strong normalisation for second order classical natural deduction, A Selective CPS Transformation, Comparing Control Constructs by Double-barrelled CPS Transforms, On the unity of duality, European Summer Meeting of the Association for Symbolic Logic, Hull, 1986, Unnamed Item, Intersection Types and Computational Rules, Unnamed Item, Unnamed Item, A partial evaluator for the untyped lambda-calculus, Equivalence in functional languages with effects, Unnamed Item, Unnamed Item, Completeness of continuation models for $\lambda_\mu$-calculus, Call-by-value Solvability, Formal polytypic programs and proofs, A Context-based Approach to Proving Termination of Evaluation, Quantifiers in Japanese, Proving the correctness of recursion-based automatic program transformations, Reasoning About Call-by-need by Means of Types, Unnamed Item, The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus, An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form, A Fresh Look at the λ-Calculus, A Process-Model for Linear Programs, The λ-calculus in the π-calculus, Unnamed Item, Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages, Small-step and big-step semantics for call-by-need, From Reduction-Based to Reduction-Free Normalization, The Simple Type Theory of Normalisation by Evaluation, Syntactic Theories in Practice, Continuation passing style for effect handlers, A functional correspondence between monadic evaluators and abstract machines for languages with computational effects, Representing Control: a Study of the CPS Transformation, Order-enriched categorical models of the classical sequent calculus, A structural approach to reversible computation, Access Control in a Core Calculus of Dependency, A Framework for Defining Logical Frameworks, A categorical understanding of environment machines, Complete Laziness: a Natural Semantics, Computational Soundness of a Call by Name Calculus of Recursively-scoped Records, Delimited control and computational effects

Uses Software

ALGOL 60

Cites Work

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