Proof theory and computer programming

DOI10.1002/MALQ.19900360505MaRDI QIDQ3032255zbMATH OpenOpenAlexFDO

Authors Ruy J. G. B. de Queiroz, Tim 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)

Recommendations

• scientific article; zbMATH DE number 2077110
• HYBRID PARTIAL-TOTAL TYPE THEORY
• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• Do-it-yourself type theory
• Constructive Mathematics and Functional Programming (Abstract)

Cited in

(10)

• A Proof-Theoretic Account of Programming and the Role of Reduction Rules
• Theorem proving method and the computer science
• Extending the Curry-Howard interpretation to linear, relevant and other resource logics
• scientific article; zbMATH DE number 1424052 (Why is no real title available?)
• Proofs and programs
• On reduction rules, meaning-as-use, and proof-theoretic semantics
• HYBRID PARTIAL-TOTAL TYPE THEORY
• Program testing and the meaning explanations of intuitionistic type theory
• Infinite objects in type theory
• Constructing recursion operators in intuitionistic type theory

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

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