Skip to content

@CoqHott The CoqHott project

Change the repository type filter

All

    Repositories list

    22 repositories

    • logrel-coq

      Public
      Logical Relation for MLTT in Coq
      Coq
      •
      MIT License
      •5•27•0•0•Updated Nov 26, 2025Nov 26, 2025

    • coq-partialfun

      Public
      Dependent composable partial functions for free in Coq
      Coq
      •
      MIT License
      •2•0•0•0•Updated Sep 3, 2025Sep 3, 2025

    • logrel-mltt

      Public
      A Logical Relation for Martin-Löf Type Theory in Agda
      HTML
      •
      MIT License
      •11•10•0•0•Updated Jul 31, 2025Jul 31, 2025

    • coqdocjs

      Public
      Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]
      JavaScript
      •
      BSD 2-Clause "Simplified" License
      •20•0•0•0•Updated Apr 17, 2025Apr 17, 2025

    • logrel-coq-cpp24

      Public
      Coq
      •0•0•0•0•Updated Dec 11, 2023Dec 11, 2023

    • parametricity-a-la-carte

      Public
      mixing CoqEAL and univalent parametricity
      Coq
      •2•4•0•0•Updated Nov 5, 2021Nov 5, 2021

    • seminar-setoid

      Public
      Toy implementation of TT^obs for the Gallinette Seminar
      Agda
      •0•0•0•0•Updated Oct 13, 2021Oct 13, 2021

    • coq-forcing

      Public
      A plugin for Coq that implements the call-by-name forcing translation
      Coq
      •3•12•5•3•Updated Jun 5, 2021Jun 5, 2021

    • cubical_forcing

      Public
      forcing on the cube category to realize univalence
      Coq
      •1•2•0•1•Updated Feb 16, 2021Feb 16, 2021

    • univalent_parametricity

      Public
      Univalent Parametricity for Effective Transport
      Coq
      •2•8•0•0•Updated Feb 1, 2021Feb 1, 2021

    • exceptional-tt

      Public
      A Coq plugin that implements exceptions in Coq
      OCaml
      •
      Do What The F*ck You Want To Public License
      •4•13•0•0•Updated Jan 7, 2021Jan 7, 2021

    • ceps

      Public
      Coq Enhancement Proposals
      36•0•0•0•Updated Jan 6, 2021Jan 6, 2021

    • coq-2ltt

      Public
      Two-level type theory in Coq
      Coq
      •1•1•0•0•Updated Aug 4, 2020Aug 4, 2020

    • coq

      Public
      Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
      OCaml
      •
      GNU Lesser General Public License v2.1
      •702•0•0•0•Updated Sep 26, 2019Sep 26, 2019

    • sProp

      Public
      repository containing the examples of the POPL paper
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•2•0•0•Updated Dec 13, 2018Dec 13, 2018

    • template-coq-forcing

      Public
      A call-by-name forcing translation implemented in Meta Coq
      Coq
      •0•0•0•0•Updated Nov 12, 2018Nov 12, 2018

    • reedy

      Public
      A formalisation of some results on theory of Reedy fibrant diagrams in two-level type theory
      Coq
      •0•0•0•0•Updated Oct 11, 2018Oct 11, 2018

    • inductive-families-extraction

      Public
      Coq
      •0•0•0•0•Updated Jan 17, 2018Jan 17, 2018

    • DICoq

      Public
      Dependent Interoperability for Coq
      Coq
      •1•8•0•0•Updated Dec 6, 2017Dec 6, 2017

    • coq-effects

      Public
      A program translation implementing self-algebraic effects in Coq.
      Coq
      •
      Do What The F*ck You Want To Public License
      •0•7•1•0•Updated Oct 14, 2017Oct 14, 2017

    • model-structures-Coq

      Public
      Formalization of a model structure on the universe of Types in Coq
      Coq
      •1•2•0•0•Updated Apr 15, 2017Apr 15, 2017

    • Program-translations-CC-omega

      Public
      Coq
      •1•13•0•0•Updated Nov 23, 2016Nov 23, 2016