Commit 0f8af4e4 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Update README with a link to the article (the HAL version for now)

parent d6dbbbc0
......@@ -90,9 +90,19 @@ knowledge of the CeCILL-B license and that you accept its terms.
make test
#+END_SRC
* Further reading
Sigmaid is described in [[https://hal.inria.fr/hal-01097444][this article]].
The Dedukti files presented there are:
- [[file:dk_domain.dk][=dk_domain.dk=]] corresponding to Section 4.1.1 (Domains),
- [[file:dk_type.dk][=dk_type.dk=]] corresponding to the other definitions and proofs of Section 4.1 (Encoding of types),
- [[file:dk_obj.dk][=dk_obj.dk=]] corresponding to Sections 4.2 (Encoding of terms) and 5.1 (Modified rewrite system)
The file [[file:coq_obj.v][=coq_obj.v=]] contains the definitions and proofs of the terminating encoding (Section 4) in Coq.
The inconsistency result of Section 4.3.4 is proved in [[file:coq_obj_inconsistency.v][=coq_obj_inconsistency.v=]].
* Author
Sigmaid is written by [[https://who.rocq.inria.fr/Raphael.Cauderlier/][Raphaël Cauderlier]].
* Footnotes
[1] Martin Abadi and Luca Cardelli, /A Theory of Objects/, Monographs in Computer Science, 1996
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment