yforster

Researcher in the Cambium Team at Inria Paris

InriaParis

Pinned Repositories

certicoq
A Verified Compiler for Gallina, Written in Gallina
Language:Coq133 14 1323
metacoq
Metaprogramming, verified meta-theory and implementation of Coq in Coq
Language:Coq358 17 14978
certicoq
Language:Coq1 2 00
coq-kolmogorov-complexity
Language:Coq1 3 00
coq-synthetic-computability
Language:Coq6 3 00
coq-verified-extraction
Language:Coq4 5 13
coqsetup
How to setup Coq quickly
4 3 00
coqtheorem
A LaTeX package to make theorem names link to coqdoc webpages. Works with ntheorem, amsthm and the LLNCS and LIPIcs classes.
Language:TeX14 3 43
stlc-norm
Proof that STLC is normalizing in Fstar
Language:Coq5 6 00
thesis-template
A LaTeX template for Bachelor or Master theses
Language:TeX7 3 05

yforster's Repositories

yforster/thesis-template
A LaTeX template for Bachelor or Master theses
Language:TeX7 3 05
yforster/coq-synthetic-computability
Language:Coq6 3 00
yforster/coq-verified-extraction
Language:Coq4 5 13
yforster/certicoq
Language:Coq1 2 00
yforster/coq-kolmogorov-complexity
Language:Coq1 3 00
yforster/dockercoq
Language:Dockerfile1 3 01
yforster/links
1 3 00
yforster/towards-fording
Language:Coq1 3 0
yforster/autoinduct
Taking a fun tactic implemented in class, and making it public for further refinement
yforster/autosubst2-1
Official repository of the Autosubst 2 project.
Language:Haskell2 0
yforster/ceps
Coq Enhancement Proposals
1 0
yforster/Certicoq_test2_add10
Language:C2 0
yforster/coq
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.
Language:OCaml3 0
yforster/coq-ceres
Coq library for serialization to S-expressions
Language:Coq
yforster/Coq-Equations
A function definition package for Coq
1
yforster/coq-library-fol
Language:Coq1 0
yforster/coq-library-undecidability
A library of formalised undecidable problems in Coq
Language:Coq3 0
yforster/coq-tricks
Tricks you wish the Coq manual told you
Language:Coq1 0
yforster/coqdocjs
Language:JavaScript
yforster/cs420-library
Language:Coq3 0
yforster/logrel-coq
Logical Relation for MLTT in Coq
Language:Coq1 0
yforster/malfunction
Malfunctional Programming
Language:OCaml1 0
yforster/malfunction-malfunctioning
Language:OCaml2 0
yforster/metacoq-guard
Language:Coq
yforster/MLTT-and-CT
Language:TeX1
yforster/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
Language:JavaScript3 0
yforster/platform
Preliminary / experimental version of the Coq platform discussed in the coq-dev maling list.
Language:Shell2 0
yforster/run-autosubst
2 02
yforster/template-coq
Reflection library for Coq
Language:OCaml3 0
yforster/test2