GitHub - fsieczkowski/Refocusing: A formalisation of the refocusing transformation by Danvy et al. in Coq

fsieczkowski / Refocusing Public

Notifications You must be signed in to change notification settings
Fork 2
Star 3

A formalisation of the refocusing transformation by Danvy et al. in Coq

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 12 Commits
environments		environments
substitutions		substitutions
substitutions_cs		substitutions_cs
substitutions_trace		substitutions_trace
utils		utils
Makefile		Makefile
README		README

Repository files navigation

==================================================
THE FORMALISATION OF THE REFOCUSING TRANSFORMATION
by Filip Sieczkowski, University of Wrocław
July 2010
==================================================

The source can be compiled using 'make'. It is known to compile correctly using
Coq 8.2pl1.

Each part of the formalisation depends on the utils/Util module.
The dependencies inside each part of the formalisation are as follows:
1. refocusing_lang
2. refocusing_signatures
3. refocusing_substitutions (or refocusing_environments)
4. case studies