Skip to main content

3 Result(s)

within Colin Rothgang Remove this filter

and

  1. Chapter and Conference Paper

    Theorem Proving in Dependently-Typed Higher-Order Logic

    Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Depende...

    Colin Rothgang, Florian Rabe, Christoph Benzmüller in Automated Deduction – CADE 29 (2023)

    Download PDF (560 KB) View Chapter

  2. No Access

    Chapter and Conference Paper

    A New Export of the Mizar Mathematical Library

    The Mizar Mathematical Library (MML) is a prime target of library exports, i.e., translations of proof assistant libraries that make the libraries available to knowledge management systems or other deduction s...

    Colin Rothgang, Artur Korniłowicz, Florian Rabe in Intelligent Computer Mathematics (2021)

  3. No Access

    Chapter and Conference Paper

    Representing Structural Language Features in Formal Meta-languages

    Structural language features are those that introduce new kinds of declarations as opposed to those that only add expressions. They pose a significant challenge when representing languages in meta-languages su...

    Dennis Müller, Florian Rabe, Colin Rothgang… in Intelligent Computer Mathematics (2020)