theories/lang.v
-R theories iris_internal_logic

# iris-curry-howard
The *Curry-Howard correspondence* defines a relationship between programming languages and logical systems.
Types correspond to propositions; programs correspond to proofs.
[*Iris*](https://iris-project.org/) is a logic designed for reasoning about the behavior of concurrent programs.
So if we apply the Curry-Howard correspondence to Iris, we should be able to prove the behavior of programs... by writing more programs.
This project is an exploration of that idea.

# KNOWNTARGETS will not be passed along to CoqMakefile
KNOWNTARGETS := CoqMakefile
# KNOWNFILES will not get implicit targets from the final rule, and so
# depending on them won't invoke the submake
# Warning: These files get declared as PHONY, so any targets depending
# on them always get rebuilt
KNOWNFILES   := Makefile _CoqProject
.DEFAULT_GOAL := invoke-coqmakefile
CoqMakefile: Makefile _CoqProject
	$(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile
invoke-coqmakefile: CoqMakefile
	$(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
.PHONY: invoke-coqmakefile $(KNOWNFILES)
####################################################################
##                      Your targets here                         ##
####################################################################
# This should be the last rule, to handle any targets not declared above
%: invoke-coqmakefile
	@true

.git
.DS_Store
CoqMakefile
CoqMakefile.conf
*.vo
*.vos
*.vok
*.glob
*.aux
*.d