Formalising formulas-as-types-as-objects

DOI10.1007/3-540-44557-9_11MaRDI QIDQ2766808zbMATH OpenFDO

Authors Haiyan Qiao

Publication date 8 July 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44557-9_11

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Structure of proofs (03F07) Second- and higher-order arithmetic and fragments (03F35) Categorical logic, topoi (03G30) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15)

Recommendations

• An Extension of the Formulas-as-Types Paradigm
• A type-free formalization of mathematics where proofs are objects
• Formalising Mathematics in Simple Type Theory
• scientific article; zbMATH DE number 960927
• Faithfully reflecting the structure of informal mathematical proofs into formal type theories
• Type theory and formalisation of mathematics
• scientific article; zbMATH DE number 1501611
• Object-oriented concepts and proof rules: Formalization in type theory and implementation in Yarrow
• A relational formulation of the theory of types
• New Computational Paradigms

Cited in

(7)

• Indexed induction-recursion
• scientific article; zbMATH DE number 6721685 (Why is no real title available?)
• A theory independent Curry-De Bruijn-Howard correspondence
• One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations
• An Extension of the Formulas-as-Types Paradigm
• Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
• A comparison of HOL and ALF formalizations of a categorical coherence theorem

This page was built for publication: Formalising formulas-as-types-as-objects

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