A Proof-Theoretic Account of Programming and the Role of Reduction Rules

DOI10.1111/J.1746-8361.1988.TB00919.XMaRDI QIDQ3830972zbMATH OpenOpenAlexWikidataFDO

Authors Ruy J. G. B. Queiroz

Publication date 1988

Published in Dialectica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1111/j.1746-8361.1988.tb00919.x

zbMATH Keywords

description of logical connectivesintroduction rulesintuitionistic type theorymeasuringnatural deductionreduction rules

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On reduction rules, meaning-as-use, and proof-theoretic semantics
• Eliminating proofs from programs
• Proof theory and computer programming
• A proof-theoretic treatment of \(\lambda \)-reduction with cut-elimination: \(\lambda \)-calculus as a logic programming language
• scientific article; zbMATH DE number 4006266

Cited in

(10)

• On reduction rules, meaning-as-use, and proof-theoretic semantics
• Proof-functional connectives and realizability
• Proof-theoretic reduction as a philosopher's tool
• Reducing Behavioural to Structural Properties of Programs with Procedures
• Extending the Curry-Howard interpretation to linear, relevant and other resource logics
• The functional interpretation of direct computations
• Natural Deduction for Equality: The Missing Entity
• A theory of reduced and minimal procedural dependencies
• Reasoning about TSO programs using reduction and abstraction
• Computational paths -- a weak groupoid

This page was built for publication: A Proof-Theoretic Account of Programming and the Role of Reduction Rules

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3830972)