Pinned Repositories
admissible-initial
Initial Semantics for admissible operations
AutoCorres
changes to autocorres 1.6
bell-quantum-experiment
Article explaining bell's violation of the inequalities
binding-debruijn
Initial semantics (de Bruijn) for binding signature
diagrammatic-resoning-spec
Specification of a diagrammatic reasoning tool
graph-editor-web
An online graph editor written in Elm
sedlex-menhir
Small example: sedlex-menhir vs ocamllex-ocamlyacc
Skew-Monoidalcategories
Skew monoidal categories in UniMath with structural strengths
unification
Notes (and implementation) of unification with binders
UniversalII
with UIP and rewrite rules in agda
amblafont's Repositories
amblafont/unification
Notes (and implementation) of unification with binders
amblafont/sedlex-menhir
Small example: sedlex-menhir vs ocamllex-ocamlyacc
amblafont/graph-editor-web
An online graph editor written in Elm
amblafont/UniversalII
with UIP and rewrite rules in agda
amblafont/diagrammatic-resoning-spec
Specification of a diagrammatic reasoning tool
amblafont/binding-debruijn
Initial semantics (de Bruijn) for binding signature
amblafont/Skew-Monoidalcategories
Skew monoidal categories in UniMath with structural strengths
amblafont/admissible-initial
Initial Semantics for admissible operations
amblafont/cogent
Proof-Code Cogeneration
amblafont/dargent-examples
Dargent layout specs in cogent
amblafont/notes
Some notes about various stuff
amblafont/thomas
The article with Thomas
amblafont/agda-stdlib
The Agda standard library
amblafont/amblafont.github.io
Personal webpage
amblafont/app-switcher
Switch between app based on a custom tree path
amblafont/coq-lsp
Visual Studio Code Extension and Language Server Protocol for Coq
amblafont/debruijn-supplements
amblafont/elm-language-server
Language server implementation for Elm
amblafont/essai-electron
amblafont/largecatmodules
Large category of modules over monads on top of UniMaths and Display category
amblafont/omegatt-agda
amblafont/play-on-damper
A script that plays an audio file as long as the (MIDI) damper is pressed
amblafont/slides
One repo to rule them all: slides for various conferences
amblafont/Smoosic
A music notation editor written in javascript
amblafont/subtyping
Towards generic subtyping implementation
amblafont/these-slides
Slides pour la thèse
amblafont/timer-driver-cogent
A formally verified timer driver using cogent
amblafont/vscode-coreact-yade
The vscode extension for the coreact yade diagram editor
amblafont/vscode-yade-example
Example of use of the vscode extension for the Coreact diagram editor
amblafont/weak-cat-type
A typing system for weak infiny groupoids