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

`Meaning-As-USE' Type Theoryconstructive infinityfixpoint operatorhigher-order typesimplementation of a type in terms of anotherIntuitionistic Type Theoryproof theorysecond-order normalisationuniverseswell- orderings

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

(11)

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

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)