GitHub - lukaszcz/clc: Confluence of an Extension of Combinatory Logic by Boolean Constants: a formalisation of the solution to the RTA open problem 15.

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 2 Commits
.gitignore		.gitignore
Makefile		Makefile
README		README
Reconstr.v		Reconstr.v
acommute.v		acommute.v
aexpand.v		aexpand.v
ared.v		ared.v
astd.v		astd.v
aux.v		aux.v
basic_defs.v		basic_defs.v
central_lemma.v		central_lemma.v
clc.v		clc.v
contraction.v		contraction.v
erase_facts.v		erase_facts.v
erasure.v		erasure.v
expansion.v		expansion.v
general.v		general.v
icommute.v		icommute.v
icontr.v		icontr.v
ired.v		ired.v
istd.v		istd.v
iterms.v		iterms.v
list_facts.v		list_facts.v
lterms.v		lterms.v
red.v		red.v
sexpand.v		sexpand.v
sexpand_std.v		sexpand_std.v
smred.v		smred.v
sn.v		sn.v
sred.v		sred.v
standard.v		standard.v
subterms.v		subterms.v
svars.v		svars.v

Repository files navigation

This is a formalisation of the confluence result from the paper:
L. Czajka "Confluence of an extension of Combinatory Logic by Boolean
constants", FSCD 2017.

The basic definitions of terms, the rewrite relations of CL-pc,
CL-pc^1, etc., are contained in the file basic_defs.v. The main
theorem is in the file clc.v. The statement of the main theorem uses
only the definitions from basic_defs.v. Everything else is needed just
to carry out the proof. In the formalisation the system CL-pc from the
paper is referred to as CLC0, the system CL-pc^1 as CLC, and CL-pc^L
as CLC+.

To compile the project type:

   make -j n

where n is the number of jobs to execute in parallel.

You need Coq version *exactly* 8.6. The proof scripts may not work
with other versions.

Note that because the proof scripts make heavy use of automated
reasoning tactics, compilation may take some time. On a machine with
eight 3.4GHz cores and 32GB of RAM, parallel compilation takes about
10 minutes. On the same machine sequential compilation takes about 25
minutes.