Head linear reduction and pure proof net extraction

DOI10.1016/0304-3975(94)90263-1zbMath0834.68104OpenAlexW2065246392MaRDI QIDQ1342250

G. F. Mascari, Marco Pedicini

Publication date: 11 January 1995

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

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

zbMATH Keywords

proof net calculus

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Logic programming (68N17) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (9)

Execution time of λ-terms via denotational semantics and intersection types ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ The relational model is injective for multiplicative exponential linear logic (without weakenings) ⋮ Tight typings and split bounds, fully developed ⋮ Towards a geometry of recursion ⋮ Evaluating lambda terms with traversals ⋮ Taming Modal Impredicativity: Superlazy Reduction ⋮ An algebraic view of the Böhm-out technique ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• On the \(\pi\)-calculus and linear logic
• Explicit substitutions

This page was built for publication: Head linear reduction and pure proof net extraction