Distilling abstract machines

DOI10.1145/2628136.2628154zbMath1345.68036arXiv1406.2370OpenAlexW2024902159MaRDI QIDQ2819700

Pablo Barenbaum, Beniamino Accattoli, Damiano Mazza

Publication date: 29 September 2016

Published in: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1406.2370

zbMATH Keywords

linear logicexplicit substitutionslambda-calculusabstract machinescall-by-needlinear head reduction

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items (20)

The Negligible and Yet Subtle Cost of Pattern Matching ⋮ Unification for $$\lambda $$ -calculi Without Propagation Rules ⋮ On the value of variables ⋮ Unnamed Item ⋮ Abstract machines, optimal reduction, and streams ⋮ Proof nets and the call-by-value \(\lambda\)-calculus ⋮ A strong call-by-need calculus ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ Node Replication: Theory And Practice ⋮ The spirit of node replication ⋮ A strong bisimulation for a classical term calculus ⋮ Classical By-Need ⋮ Unnamed Item ⋮ Reasonable space for the \(\lambda \)-calculus, logarithmically ⋮ Exponentials as substitutions and the cost of cut elimination in linear logic ⋮ Preorder-constrained simulations for program refinement with effects ⋮ Reasoning About Call-by-need by Means of Types ⋮ The Useful MAM, a Reasonable Implementation of the Strong $$\lambda $$ -Calculus ⋮ A Fresh Look at the λ-Calculus ⋮ (In)efficiency and reasonable cost models

This page was built for publication: Distilling abstract machines