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 (only showing first 100 items - show all)

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

Uses Software

ALGOL 60

Cites Work

This page was built for publication: Call-by-name, call-by-value and the \(\lambda\)-calculus