5
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Isabelle/Spartan -- A Dependent Type Theory Framework for Isabelle

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          This paper introduces Isabelle/Spartan, an implementation of intensional dependent type theory with cumulative universes as an object logic in the Isabelle proof assistant. In contrast to other systems supporting dependent type theory, Isabelle is based on simple type theory -- yet I show how its existing logical framework infrastructure is able to handle automation tasks that are typically implemented on the source code level of dependently-typed systems. I also go some way in integrating the propositions-as-types paradigm with the declarative Isar proof language. Isabelle/Spartan supports book HoTT and the univalence axiom, and its capabilities are demonstrated by the formalization of foundational results from the Homotopy Type Theory book.

          Related collections

          Author and article information

          Journal
          14 February 2020
          Article
          2002.09282
          09276886-b96a-4df1-adfc-6c055d73f4e8

          http://arxiv.org/licenses/nonexclusive-distrib/1.0/

          Custom metadata
          15 pages
          cs.LO

          Theoretical computer science

          Comments

          Comment on this article