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.
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.
gym-numgrid
An OpenAI Gym environment where an agent explores a grid of hand-written digits images.
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/coq-actema
Coq plugin integrating Actema as a tactic.
Champitoad/gym-numgrid
An OpenAI Gym environment where an agent explores a grid of hand-written digits images.
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/apparatus
A hybrid graphics editor and programming environment for creating interactive diagrams.
Champitoad/coq-plugin-template-atdgen
Template of Coq Plugin using the Dune build system, and showcasing some advanced features
Champitoad/dotfiles
Champitoad/dvdtyp
Template for research notes.
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/mathlib4
The math library of Lean 4
Champitoad/msca-pf
LaTeX class and template for Marie Skłodowska-Curie Actions Postdoctoral Fellow (MSCA-PF) grant applications
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/Scrollify
A jQuery plugin that assists scrolling and snaps to sections.
Champitoad/thesis
My PhD thesis!
Champitoad/typst-slides
A bunch of slide decks written in Typst with the Polylux library.
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.