Pinned Repositories
3I013
Projet de recherche pour l'UE 3I013 de la L3 Informatique de l'UPMC.
actema-desktop
Desktop/Electron version of Actema, to be run with a plugin for a proof assistant.
aLCE
aLCE est une application permettant de jouer au Cadavre Exquis avec ses amis à partir d'un terminal Android.
cbpv
A study of a simplified Call-By-Push-Value lambda-calculus in Coq.
CoqHopf
Construction of the Hopf fibration in Homotopy Type Theory, using the HoTT library for Coq.
flower-auto
Can ❀ decide intuitionistic propositional logic?
flower-prover
Can 🌸 be turned into a direct manipulation GUI for theorem proving?
flowers-metatheory
Can ✿ capture intuitionistic logic?
focalisation-classical-realizability
Présentation de l'article Focalisation and Classical Realizability de Guillaume Munch-Maccagnoni.
LambdaSub
Formalization in Coq of a simply typed λ-calculus extended with records and subtyping.
Champitoad's Repositories
Champitoad/flower-prover
Can 🌸 be turned into a direct manipulation GUI for theorem proving?
Champitoad/cbpv
A study of a simplified Call-By-Push-Value lambda-calculus in Coq.
Champitoad/CoqHopf
Construction of the Hopf fibration in Homotopy Type Theory, using the HoTT library for Coq.
Champitoad/flower-auto
Can ❀ decide intuitionistic propositional logic?
Champitoad/flowers-metatheory
Can ✿ capture intuitionistic logic?
Champitoad/focalisation-classical-realizability
Présentation de l'article Focalisation and Classical Realizability de Guillaume Munch-Maccagnoni.
Champitoad/LambdaSub
Formalization in Coq of a simply typed λ-calculus extended with records and subtyping.
Champitoad/3I013
Projet de recherche pour l'UE 3I013 de la L3 Informatique de l'UPMC.
Champitoad/actema-desktop
Desktop/Electron version of Actema, to be run with a plugin for a proof assistant.
Champitoad/aLCE
aLCE est une application permettant de jouer au Cadavre Exquis avec ses amis à partir d'un terminal Android.
Champitoad/Bi0Cube
Arduino code, Python scripts and website controlling the Bi0Cube PPE.
Champitoad/coq-actema
Coq plugin integrating Actema as a tactic.
Champitoad/memoir-lophisc
Mémoire de M1 du master LOPHISC.
Champitoad/term-lnets
Towards a term syntax for L-nets ("Travail de Recherche Encadré" realized as part of the M1 MPRI curriculum).
Champitoad/coq-plugin-template-atdgen
Template of Coq Plugin using the Dune build system, and showcasing some advanced features
Champitoad/dotfiles
Champitoad/gym-numgrid
An OpenAI Gym environment where an agent explores a grid of hand-written digits images.
Champitoad/IExSwarm
Android remote control application for the IExSwarm robot.
Champitoad/kaobook
A LaTeX class for books, reports or theses based on https://github.com/kenohori/thesis and https://github.com/Tufte-LaTeX/tufte-latex.
Champitoad/large-star-collider
Stellar resolution implemented with interactive execution
Champitoad/pablo.donato
My personal website
Champitoad/panda2prftree
Convert natural deduction proofs saved in Panda xml format to LaTeX prftree format.
Champitoad/radial-menu-vue
Radial Menu Component in Vue.js
Champitoad/RGB-Run
RGB Run is a minimalist, yet hard to master runner game with gameplay focused on RGB colors switching.
Champitoad/Scrollify
A jQuery plugin that assists scrolling and snaps to sections.
Champitoad/Taquin
Un projet de jeu de taquin pour le module IHM de 1ère année de DUT Informatique.
Champitoad/thesis
My PhD thesis!
Champitoad/vim-abolish
abolish.vim: easily search for, substitute, and abbreviate multiple variants of a word
Champitoad/vscode-ocaml
An extension for VS Code which provides support for the OCaml language.
Champitoad/wpm
A feature-rich wallpaper manager written in Bash.