Lyon, France

Kazuhiko Sakaguchi

Expert
@pi8027

Postdoc in the Plume team | Interests: interactive theorem proving, formalization of mathematics, proof by reflection, and parametricity

lambda-calculus. A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2

88

typeinfer. Type inference in OCaml

40

stablesort. Stable sort algorithms and their stability proofs in Rocq

25

efficient-finfun. Coq

13

formalized-postscript. PostScript programming in the Coq proof assistant

13

pane-maximize. maximize/restore panes in tmux 1.7.

9

vass. Coq

4

sandpit. Coq

3

config. my configuration files

3

opam-repository. Main public package repository for OPAM, the source package manager of OCaml.

1

math-comp. Mathematical Components

1

analysis. Mathematical Components compliant Analysis Library

1

record-expansion. A translation from Coq to Coq expanding and eliminating records (WIP)

1
13
Apply