Skip to content
@CoqHott

The CoqHott project

Popular repositories Loading

  1. logrel-coq logrel-coq Public

    Logical Relation for MLTT in Coq

    Coq 20 3

  2. Program-translations-CC-omega Program-translations-CC-omega Public

    Coq 13 1

  3. exceptional-tt exceptional-tt Public

    A Coq plugin that implements exceptions in Coq

    OCaml 13 4

  4. coq-forcing coq-forcing Public

    A plugin for Coq that implements the call-by-name forcing translation

    Coq 12 3

  5. DICoq DICoq Public

    Dependent Interoperability for Coq

    Coq 8 1

  6. univalent_parametricity univalent_parametricity Public

    Univalent Parametricity for Effective Transport

    Coq 8 2

Repositories

Showing 10 of 22 repositories
  • logrel-coq Public

    Logical Relation for MLTT in Coq

    CoqHott/logrel-coq’s past year of commit activity
    Coq 20 MIT 3 0 1 Updated Dec 21, 2024
  • coq-partialfun Public Forked from TheoWinterhalter/coq-partialfun

    Dependent composable partial functions for free in Coq

    CoqHott/coq-partialfun’s past year of commit activity
    Coq 0 MIT 2 0 0 Updated Nov 11, 2024
  • coqdocjs Public Forked from coq-community/coqdocjs

    Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]

    CoqHott/coqdocjs’s past year of commit activity
    JavaScript 0 BSD-2-Clause 17 0 0 Updated Aug 23, 2024
  • logrel-mltt Public Forked from mr-ohman/logrel-mltt

    A Logical Relation for Martin-Löf Type Theory in Agda

    CoqHott/logrel-mltt’s past year of commit activity
    HTML 7 MIT 11 0 0 Updated May 7, 2024
  • logrel-coq-cpp24 Public
    CoqHott/logrel-coq-cpp24’s past year of commit activity
    Coq 0 0 0 0 Updated Dec 11, 2023
  • parametricity-a-la-carte Public

    mixing CoqEAL and univalent parametricity

    CoqHott/parametricity-a-la-carte’s past year of commit activity
    Coq 4 2 0 0 Updated Nov 5, 2021
  • seminar-setoid Public

    Toy implementation of TT^obs for the Gallinette Seminar

    CoqHott/seminar-setoid’s past year of commit activity
    Agda 0 0 0 0 Updated Oct 13, 2021
  • coq-forcing Public

    A plugin for Coq that implements the call-by-name forcing translation

    CoqHott/coq-forcing’s past year of commit activity
    Coq 12 3 5 3 Updated Jun 5, 2021
  • cubical_forcing Public

    forcing on the cube category to realize univalence

    CoqHott/cubical_forcing’s past year of commit activity
    Coq 2 1 0 1 Updated Feb 16, 2021
  • univalent_parametricity Public

    Univalent Parametricity for Effective Transport

    CoqHott/univalent_parametricity’s past year of commit activity
    Coq 8 2 0 0 Updated Feb 1, 2021
View all repositories

Top languages

Loading…

Most used topics

Loading…