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

DOI10.1111/j.1746-8361.1988.tb00919.xzbMath0676.03007OpenAlexW1971091241WikidataQ56050816 ScholiaQ56050816MaRDI QIDQ3830972

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

natural deductionintuitionistic type theoryintroduction rulesreduction rulesmeasuringdescription of logical connectives

Mathematics Subject Classification ID

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

Related Items

Extending the Curry-Howard interpretation to linear, relevant and other resource logics ⋮ The Functional Interpretation of Direct Computations ⋮ On reduction rules, meaning-as-use, and proof-theoretic semantics ⋮ Natural Deduction for Equality: The Missing Entity

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