
TL;DR
This paper discusses type inference mechanisms in programming languages and their application in interactive theorem proving, focusing on the Mathematical Components project for verifying complex mathematical theorems.
Contribution
It explains specific type inference techniques used in the Mathematical Components project for formal verification of the Feit-Thompson theorem.
Findings
Type inference aids in automating theorem proving processes.
Mechanisms improve the efficiency of formal verification.
Application to the Feit-Thompson theorem demonstrates practical utility.
Abstract
In the theory of programming languages, type inference is the process of inferring the type of an expression automatically, often making use of information from the context in which the expression appears. Such mechanisms turn out to be extremely useful in the practice of interactive theorem proving, whereby users interact with a computational proof assistant to construct formal axiomatic derivations of mathematical theorems. This article explains some of the mechanisms for type inference used by the Mathematical Components project, which is working towards a verification of the Feit-Thompson theorem.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematics, Computing, and Information Processing · Semantic Web and Ontologies
