La théorie intuitionniste des types : sémantique des preuves et théorie des constructions

DOI10.1017/S0012217300009537zbMATH Open0923.03067MaRDI QIDQ4252873FDOQ4252873

Authors: Michel Bourdeau 

Publication date: 22 June 1999

Published in: Dialogue (Search for Journal in Brave)

Recommendations

• scientific article; zbMATH DE number 4096759
• Treatise on intuitionistic type theory
• scientific article; zbMATH DE number 2077110
• AN INTERPRETATION OF MARTIN‐LÖF'S CONSTRUCTIVE THEORY OF TYPES IN ELEMENTARY TOPOS THEORY
• Constructive theory of sets with types; compatibility with Church's thesis

zbMATH Keywords

constructive type theoryproof objectsproof processes

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35) Intuitionistic mathematics (03F55)

Cited In (25)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Foundations of mathematics in polymorphic type theory
• Title not available (Why is that?)
• History and philosophy of constructive type theory
• Monotone inductive definitions in a constructive theory of functions and classes
• Title not available (Why is that?)
• The constructive reference theory. \(\Sigma\) types and definite descriptions.
• Title not available (Why is that?)
• An intensional type theory: Motivation and cut-elimination
• Title not available (Why is that?)
• Interpreting descriptions in intensional type theory
• Title not available (Why is that?)
• Constructions, proofs and the meaning of logical constants
• Treatise on intuitionistic type theory
• On specifications, subset types and interpretation of proposition in type theory
• Type Theory and the Theory of Meaning
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proof-search in type-theoretic languages: An introduction
• Constructing possible worlds*
• Reflective semantics of constructive type theory
• Constructive theory of sets with types; compatibility with Church's thesis
• Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves

This page was built for publication: La théorie intuitionniste des types : sémantique des preuves et théorie des constructions

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