Proof theory and computer programming

DOI10.1002/MALQ.19900360505zbMATH Open0691.03042OpenAlexW1986417908MaRDI QIDQ3032255FDOQ3032255

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

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)

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)

Cited In (10)

• Theorem proving method and the computer science
• Extending the Curry-Howard interpretation to linear, relevant and other resource logics
• Title not available (Why is that?)
• 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
• A Proof-Theoretic Account of Programming and the Role of Reduction Rules

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)