amblafont Goto Github PK

admissible-initial

Initial Semantics for admissible operations

agda-stdlib

The Agda standard library

amblafont.github.io

Personal webpage

app-switcher

Switch between app based on a custom tree path

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

cacao2018

categorical-expression-helper

Command-line interactive tool for rewriting a morphism in a categorical setting.

chocola-03-2019

Slides

cogent

Proof-Code Cogeneration

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.

coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq

csl-presentation

slides for CSL presentation (high level signatures)

dargent-examples

Dargent layout specs in cogent

debruijn-supplements

dependent-eliminator-ind-ind-rec

Experiments with simulation of Dependent eliminator of inductive-inductive-recursive datatypes

drivegal

Photo Gallery for Google Drive

elm-language-server

Language server implementation for Elm

essai-electron

fcitx-table-latex-nix-src

nix source for latex engine (input method fcitx), starting from https://download.fcitx-im.org/fcitx-table-other/fcitx-table-other-0.2.4.tar.xz

finitary-functors

finitary functors in UniMath

graph-editor-web

An online graph editor written in Elm

guide-unimath

A guide to UniMath

hashcode

ibus-table-others

ibus-table-others

largecatmodules

Large category of modules over monads on top of UniMaths and Display category

monads

Coq code accompanying several articles on semantics of functional programming languages

nix-fcitx-latex

nix package for latex input method (using fcitx), adapted from the nix package fcitx-table-other

notes

Some notes about various stuff