diff --git a/README.md b/README.md index 4d6aa02..23349de 100644 --- a/README.md +++ b/README.md @@ -50,8 +50,8 @@ which is in turn equivalent to Streicher's Axiom K (i.e., dependent pattern matc # Accompanying material -- Most recent [draft paper](201903/compact-20190331.pdf) ([arXiv version](https://arxiv.org/pdf/1904.02809.pdf)), accepted to the 10th International Conference on - Interactive Theorem Proving (ITP 2019) +- Most recent [paper](itp2019/LIPIcs-ITP-2019-5.pdf) ([arXiv version](https://arxiv.org/pdf/1904.02809.pdf)), presented at the 10th International Conference on Interactive Theorem Proving (ITP 2019) +- ITP 2019 [slides](itp2019/slides_itp2019.pdf) - TPP 2018 slides for [LOUDS](tpp2018/slides_louds_en.pdf) and [dynamic bit vectors](tpp2018/slides_dynamic.pdf) - JSSST 2018 [draft paper](jssst2018/compact.pdf) diff --git a/itp2019/LIPIcs-ITP-2019-5.pdf b/itp2019/LIPIcs-ITP-2019-5.pdf new file mode 100644 index 0000000..c6b35c0 Binary files /dev/null and b/itp2019/LIPIcs-ITP-2019-5.pdf differ diff --git a/itp2019/slides_itp2019.pdf b/itp2019/slides_itp2019.pdf new file mode 100644 index 0000000..300b86e Binary files /dev/null and b/itp2019/slides_itp2019.pdf differ