The Functional Interpretation of Direct Computations

DOI10.1016/j.entcs.2011.03.003zbMath1347.03062OpenAlexW2026740543WikidataQ56211002 ScholiaQ56211002MaRDI QIDQ5179008

Anjolina de Oliveira, Ruy J. G. B. de Queiroz

Publication date: 18 March 2015

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2011.03.003

zbMATH Keywords

natural deductionequalitylabelled deductionequality type

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On reduction rules, meaning-as-use, and proof-theoretic semantics
• The lambda calculus, its syntax and semantics
• Constructivism in mathematics. An introduction. Volume II
• On the logic of unification
• Meaning, Function, Purpose, Usefulness, Consequences - Interconnected Concepts
• A Proof-Theoretic Account of Programming and the Role of Reduction Rules
• Extending the Curry-Howard interpretation to linear, relevant and other resource logics
• Bounds for proof-search and speed-up in the predicate calculus
• A normalization procedure for the equational fragment of labelled natural deduction
• Natural Deduction for Equality: The Missing Entity
• Finite Definability of Number‐Theoretic Functions and Parametric Completeness of Equational Calculi

This page was built for publication: The Functional Interpretation of Direct Computations