Pinned Repositories
bam
A PBT framework
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.
DeduktiEncodings
Various encoding written in Dedukti
dkP
Yet another tool for Dedukti to replace rewrite rules to equalities
dkprune
A tool to prune Dedukti files
dotfiles
my dot files
grace
A fancy diagnostics library that allows your compilers to exit with grace
kubatipo
Attempt to encode Cubical Type Theory in Dedukti
lambdapi
Minimal implementation of the λΠ-calculus modulo
lwt
OCaml promises and concurrent I/O
francoisthire's Repositories
francoisthire/bam
A PBT framework
francoisthire/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.
francoisthire/DeduktiEncodings
Various encoding written in Dedukti
francoisthire/dkP
Yet another tool for Dedukti to replace rewrite rules to equalities
francoisthire/dkprune
A tool to prune Dedukti files
francoisthire/dotfiles
my dot files
francoisthire/grace
A fancy diagnostics library that allows your compilers to exit with grace
francoisthire/kubatipo
Attempt to encode Cubical Type Theory in Dedukti
francoisthire/lambdapi
Minimal implementation of the λΠ-calculus modulo
francoisthire/lwt
OCaml promises and concurrent I/O
francoisthire/matita
Matita (proof assistant) with embedded elpi
francoisthire/rust
a safe, concurrent, practical language
francoisthire/opam-repository
Main public package repository for opam, the source package manager of OCaml.
francoisthire/SharingAnArithmeticLibrary
This repository presents an arithmetic library that is shared between several proof systems
francoisthire/sttforall
An implementation of the sttforall logic
francoisthire/teztnets
Repository for the setup of the Tezos test network infrastructure
francoisthire/type-systems-framework
An experiment about sharing the same framework for different type systems
francoisthire/vg
Declarative 2D vector graphics for OCaml
francoisthire/XMLCoqDedukti
francoisthire/zds-coding-gouter
Ressources for the zds meeting during the french event "coding goûter"
francoisthire/zds-site
Dépot ZDS