Carnegie Mellon University
Browse
file.pdf (220.72 kB)

Type Inference in Mathematics

Download (220.72 kB)
journal contribution
posted on 2012-02-01, 00:00 authored by Jeremy AvigadJeremy Avigad

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 constructformal 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

History

Publisher Statement

Copyright the Author

Date

2012-02-01

Usage metrics

    Categories

    Keywords

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC