Proof theory and computer programming

DOI10.1002/malq.19900360505zbMath0691.03042OpenAlexW1986417908MaRDI QIDQ3032255

Ruy J. G. B. de Queiroz, Thomas S. E. Maibaum

Publication date: 1990

Published in: Zeitschrift für Mathematische Logik und Grundlagen der Mathematik (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/malq.19900360505

zbMATH Keywords

proof theoryuniverseswell- orderingshigher-order types`Meaning-As-USE' Type Theoryconstructive infinityfixpoint operatorimplementation of a type in terms of anotherIntuitionistic Type Theorysecond-order normalisation

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35)

Related Items

Extending the Curry-Howard interpretation to linear, relevant and other resource logics ⋮ On reduction rules, meaning-as-use, and proof-theoretic semantics

This page was built for publication: Proof theory and computer programming