Highlights
- Pro
-
-
flowers-metatheory Public
Can ✿ capture intuitionistic logic?
-
mathlib4 Public
Forked from leanprover-community/mathlib4The math library of Lean 4
Lean Apache License 2.0 UpdatedOct 8, 2024 -
typst-slides Public
A bunch of slide decks written in Typst with the Polylux library.
TeX Creative Commons Zero v1.0 Universal UpdatedSep 19, 2024 -
-
thesis Public
My PhD thesis!
TeX Creative Commons Attribution 4.0 International UpdatedJul 31, 2024 -
kaobook Public
Forked from fmarotta/kaobookA LaTeX class for books, reports or theses based on https://github.com/kenohori/thesis and https://github.com/Tufte-LaTeX/tufte-latex.
TeX LaTeX Project Public License v1.3c UpdatedJul 30, 2024 -
large-star-collider Public
Forked from engboris/transcendental-syntaxStellar resolution implemented with interactive execution
OCaml GNU General Public License v3.0 UpdatedJun 2, 2024 -
flower-prover Public
Can 🌸 be turned into a direct manipulation GUI for theorem proving?
-
-
actema-desktop Public
Desktop/Electron version of Actema, to be run with a plugin for a proof assistant.
Vue UpdatedJul 13, 2023 -
radial-menu-vue Public
Forked from axln/radial-menu-vueRadial Menu Component in Vue.js
Vue MIT License UpdatedNov 28, 2022 -
coq-plugin-template-atdgen Public
Forked from coq-community/coq-plugin-templateTemplate of Coq Plugin using the Dune build system, and showcasing some advanced features
-
Présentation de l'article Focalisation and Classical Realizability de Guillaume Munch-Maccagnoni.
-
term-lnets Public
Towards a term syntax for L-nets ("Travail de Recherche Encadré" realized as part of the M1 MPRI curriculum).
TeX MIT License UpdatedApr 1, 2020 -
LambdaSub Public
Formalization in Coq of a simply typed λ-calculus extended with records and subtyping.
-
CoqHopf Public
Construction of the Hopf fibration in Homotopy Type Theory, using the HoTT library for Coq.
-
-
cbpv Public
A study of a simplified Call-By-Push-Value lambda-calculus in Coq.
-
Scrollify Public
Forked from lukehaas/ScrollifyA jQuery plugin that assists scrolling and snaps to sections.
JavaScript MIT License UpdatedNov 19, 2018 -
-
wpm Public
A feature-rich wallpaper manager written in Bash.
Shell GNU General Public License v3.0 UpdatedApr 1, 2018 -
panda2prftree Public
Convert natural deduction proofs saved in Panda xml format to LaTeX prftree format.
OCaml GNU General Public License v3.0 UpdatedMar 13, 2018 -
vscode-ocaml Public
Forked from hackwaly/vscode-ocamlAn extension for VS Code which provides support for the OCaml language.
TypeScript MIT License UpdatedOct 28, 2017 -
3I013 Public
Projet de recherche pour l'UE 3I013 de la L3 Informatique de l'UPMC.
TeX UpdatedMay 3, 2017 -
gym-numgrid Public
An OpenAI Gym environment where an agent explores a grid of hand-written digits images.
Python GNU General Public License v3.0 UpdatedMay 1, 2017 -
vim-abolish Public
Forked from tpope/vim-abolishabolish.vim: easily search for, substitute, and abbreviate multiple variants of a word
Vim Script UpdatedNov 11, 2016 -
IExSwarm Public
Android remote control application for the IExSwarm robot.
-
Taquin Public
Un projet de jeu de taquin pour le module IHM de 1ère année de DUT Informatique.
Java GNU General Public License v3.0 UpdatedJul 1, 2015 -
Bi0Cube Public
Arduino code, Python scripts and website controlling the Bi0Cube PPE.
JavaScript GNU General Public License v3.0 UpdatedJan 29, 2015