Type inference in mathematics

MaRDI QIDQ4904162zbMATH OpenFDO

Authors Jeremy Avigad

Publication date 28 January 2013

Full work available at URL https://arxiv.org/abs/1111.5885

zbMATH Keywords

dependent typesproof assistantstype inference

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Theory of programming languages (68N15)

Recommendations

• Canonical structures for the working Coq user
• scientific article; zbMATH DE number 1215502
• Type inference for ZFH
• scientific article; zbMATH DE number 559219
• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L

Cited in

(6)

• Computations on types
• Symbolic abstract data type inference
• scientific article; zbMATH DE number 5994829 (Why is no real title available?)
• Type inference for ZFH
• Type Inference for Correspondence Types
• Type inference for set theory

This page was built for publication: Type inference in mathematics

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