TheoWinterhalter

Researcher, proof assistants and dependent types

Inria SaclaySaclay

Pinned Repositories

metacoq
Metaprogramming, verified meta-theory and implementation of Coq in Coq
Language:Coq357 17 14878
ssprove
A foundational framework for modular cryptographic proofs in Coq
Language:Coq53 8 610
atom-language-agda
Agda language support for the Atom editor
Language:CoffeeScript1 2 00
coq-partialfun
Dependent composable partial functions for free in Coq
Language:Coq6 2 02
ett-to-itt
Coq formalisation and plugin of a translation from ETT to ITT
Language:Coq4 5 10
ett-to-wtt
Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory
Language:Coq6 2 00
formal-type-theory
Formalising Type Theory in a modular way for translations between type theories
Language:Coq90 12 194
ghost-reflection
A formalisation of a dependent type theory with ghost types
Language:Coq01
phd-thesis
Phd Thesis of Théo Winterhalter. Look at releases to get the latest PDF.
Language:TeX30 4 02
sirtt
Shape-Irrelevant Reflection Type Theory
Language:Coq6 2 00

TheoWinterhalter's Repositories

TheoWinterhalter/formal-type-theory
Formalising Type Theory in a modular way for translations between type theories
Language:Coq90 12 194
TheoWinterhalter/phd-thesis
Phd Thesis of Théo Winterhalter. Look at releases to get the latest PDF.
Language:TeX30 4 02
TheoWinterhalter/coq-partialfun
Dependent composable partial functions for free in Coq
Language:Coq6 2 02
TheoWinterhalter/ett-to-wtt
Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory
Language:Coq6 2 00
TheoWinterhalter/sirtt
Shape-Irrelevant Reflection Type Theory
Language:Coq6 2 00
TheoWinterhalter/ett-to-itt
Coq formalisation and plugin of a translation from ETT to ITT
Language:Coq4 5 10
TheoWinterhalter/atom-language-agda
Agda language support for the Atom editor
Language:CoffeeScript1 2 00
TheoWinterhalter/resizing-reflection
Master Thesis with Nicolas Tabareau on Resizing Rules and Reflection
Language:Coq1 2 00
TheoWinterhalter/sublimeassembly
Provides actually decent code highlighting for x86-64 assembly in Sublime Text
1 2 0
TheoWinterhalter/template-coq
Reflection library for Coq
Language:Coq1 5 0
TheoWinterhalter/ghost-reflection
A formalisation of a dependent type theory with ghost types
Language:Coq01
TheoWinterhalter/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:OCaml2 0
TheoWinterhalter/FStar
Verification system for effectful programs
Language:F*1 0
TheoWinterhalter/galliblog
Implementing the Gallinette website and its blog
Language:OCaml2 0
TheoWinterhalter/kaobook
A LaTeX class for books, reports or theses based on https://github.com/kenohori/thesis and https://github.com/Tufte-LaTeX/tufte-latex.
Language:TeX1 0
TheoWinterhalter/language-prolog
Prolog language support for Atom
Language:CoffeeScript2 0
TheoWinterhalter/ocawb
Write HTML with ocaml (just fun with continuations)
Language:OCaml3 1
TheoWinterhalter/pdm4all
Partial Dijkstra monads for all
Language:Coq
TheoWinterhalter/selection-count
Add character count for atom editor
Language:CoffeeScript2 5
TheoWinterhalter/vscoq
A Visual Studio Code extension for Coq [maintainer=@maximedenes]
Language:TypeScript1 0

TheoWinterhalter

Pinned Repositories

metacoq

ssprove

atom-language-agda

coq-partialfun

ett-to-itt

ett-to-wtt

formal-type-theory

ghost-reflection

phd-thesis

sirtt

TheoWinterhalter's Repositories

TheoWinterhalter/formal-type-theory

TheoWinterhalter/phd-thesis

TheoWinterhalter/coq-partialfun

TheoWinterhalter/ett-to-wtt

TheoWinterhalter/sirtt

TheoWinterhalter/ett-to-itt

TheoWinterhalter/atom-language-agda

TheoWinterhalter/resizing-reflection

TheoWinterhalter/sublimeassembly

TheoWinterhalter/template-coq

TheoWinterhalter/ghost-reflection

TheoWinterhalter/coq

TheoWinterhalter/FStar

TheoWinterhalter/galliblog

TheoWinterhalter/kaobook

TheoWinterhalter/language-prolog

TheoWinterhalter/ocawb

TheoWinterhalter/pdm4all

TheoWinterhalter/selection-count

TheoWinterhalter/vscoq