DmxLarchey

CNRSNancy, France

Pinned Repositories

Accessibility
A small course on the inductive accessibility predicate in Coq
Language:Coq2 2 00
BFE
Certification of Breadth-First algorithms by Extraction
Language:Coq2 3 00
Combinatory-Logic-for-students
Confluence de la logique combinatoire en Coq
Language:Coq10
Coq-is-total
A proof that Coq contains any total mu-recursive function
Language:Coq4 2 00
Coq-Phase-Semantics
Coq Source for Relational Phase Semantics and Cut-elimination
Language:Coq60
Introduction-to-Coq
Introduction to the Coq proof assistant
Language:Coq5 5 00
ite-normalisation
L. Paulson's If-Then-Else normalisation algorithm in Coq via simulated Induction-Recursion
Language:Coq9 2 00
PC19
Exercices and Examples for the PC'19 Autumn school
Language:Coq40
Ramsey
Ramsey's theorem in Type Theory and applications
Language:Coq2 2 00
The-Braga-Method
The Braga Method for Extracting Certified OCaml from Coq code
Language:Coq51

DmxLarchey's Repositories

DmxLarchey/Coq-Phase-Semantics
Coq Source for Relational Phase Semantics and Cut-elimination
Language:Coq60
DmxLarchey/Introduction-to-Coq
Introduction to the Coq proof assistant
Language:Coq5 5 00
DmxLarchey/The-Braga-Method
The Braga Method for Extracting Certified OCaml from Coq code
Language:Coq51
DmxLarchey/Accessibility
A small course on the inductive accessibility predicate in Coq
Language:Coq2 2 00
DmxLarchey/Ramsey
Ramsey's theorem in Type Theory and applications
Language:Coq2 2 00
DmxLarchey/Hydra
Hercules kills the Hydra in Coq
Language:Coq11
DmxLarchey/Murec_Extraction
Extraction of µ-recursive algorithms in Coq
Language:Coq11
DmxLarchey/Tree-mirror
Tree mirroring specified in a small fun. language and Coq proofs of correctedness
Language:Coq1 2 0
DmxLarchey/wf-strict-order-finite
Direct proof that strict orders on listable types are well-founded
Language:Coq1
DmxLarchey/Breadth-First-Numbering
Coq implementation of Breadth-First Numbering à la Okasaki
Language:Coq
DmxLarchey/Coq-Kruskal
Description of the Coq-Kruskal project with a map and pointers
1 0
DmxLarchey/coq-library-undecidability
A library of formalised undecidable problems in Coq
Language:Coq
DmxLarchey/Friedman-TREE
Construction of Friedman's tree(n) and TREE(n) in Coq
Language:Coq
DmxLarchey/Karp-Miller
A Coq mechanization of the Karp-Miller algorithm based on Kruskal-AlmostFull
Language:Coq2 0
DmxLarchey/Kruskal-AlmostFull
Library of basic results about Almost Full relations in Coq
Language:Coq
DmxLarchey/Kruskal-Fan
The Fan theorem for inductive bars and a constructive variant of König's lemma
Language:Coq
DmxLarchey/Kruskal-Finite
Tools for dealing with finiteness and choice
Language:Coq
DmxLarchey/Kruskal-Higman
Detailed proof of Higman's lemma for unary trees and lists
Language:Coq
DmxLarchey/Kruskal-Stumps
Wim Veldman's stumps for almost full relations in inductive type theory
Language:Coq
DmxLarchey/Kruskal-Theorems
Kruskal and Higman type tree theorems for the Kruskal-AlmostFull library
Language:Coq
DmxLarchey/Kruskal-Trees
Coq library for rose trees
Language:Coq1
DmxLarchey/Kruskal-Veldman
An adaptation of Wim Veldman's proof of the tree theorem to Coq
Language:Coq
DmxLarchey/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
Language:OCaml
DmxLarchey/opam-repository
Main public package repository for opam, the source package manager of OCaml.
DmxLarchey/PHP-short
A short Coq proof of the PHP
Language:Coq
DmxLarchey/Quasi-Morphisms
Quasi morphisms for Almost Full relations
Language:Coq
DmxLarchey/Relevant-decidability
A constructive account of Kripke-Curry's decidability proof for Implicational Relevance logic (see README.md below)
Language:Coq2 11
DmxLarchey/shortlex
Well-foundedness of the shortlex(icographic) product
Language:Coq2 0
DmxLarchey/SQRT2
The square root of 2 is not rational
Language:Coq2 0
DmxLarchey/SystemF
A clean and short proof of strong normalization for Curry-style System F
Language:Coq2 0