Skip to content

Commit

Permalink
Deploying to web from @ 816ac17 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Jan 7, 2024
1 parent c169758 commit 2945ad0
Show file tree
Hide file tree
Showing 11 changed files with 13 additions and 13 deletions.
2 changes: 1 addition & 1 deletion Confluence/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -244,4 +244,4 @@
<a id="plfa_plfa-part2-Confluence-18860" class="Symbol">...</a> <a id="plfa_plfa-part2-Confluence-18864" class="Symbol">|</a> <a id="plfa_plfa-part2-Confluence-18866" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">⟨</a> <a id="plfa_plfa-part2-Confluence-18868" href="../Confluence/#plfa_plfa-part2-Confluence-18868" class="Bound">N</a> <a id="plfa_plfa-part2-Confluence-18870" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">,</a> <a id="plfa_plfa-part2-Confluence-18872" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">⟨</a> <a id="plfa_plfa-part2-Confluence-18874" href="../Confluence/#plfa_plfa-part2-Confluence-18874" class="Bound">M₁⇛N</a> <a id="plfa_plfa-part2-Confluence-18879" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">,</a> <a id="plfa_plfa-part2-Confluence-18881" href="../Confluence/#plfa_plfa-part2-Confluence-18881" class="Bound">M₂⇛N</a> <a id="plfa_plfa-part2-Confluence-18886" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">⟩</a> <a id="plfa_plfa-part2-Confluence-18888" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">⟩</a> <a id="plfa_plfa-part2-Confluence-18890" class="Symbol">=</a>
<a id="plfa_plfa-part2-Confluence-18898" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">⟨</a> <a id="plfa_plfa-part2-Confluence-18900" href="../Confluence/#plfa_plfa-part2-Confluence-18868" class="Bound">N</a> <a id="plfa_plfa-part2-Confluence-18902" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">,</a> <a id="plfa_plfa-part2-Confluence-18904" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">⟨</a> <a id="plfa_plfa-part2-Confluence-18906" href="../Confluence/#plfa_plfa-part2-Confluence-6833" class="Function">pars-betas</a> <a id="plfa_plfa-part2-Confluence-18917" href="../Confluence/#plfa_plfa-part2-Confluence-18874" class="Bound">M₁⇛N</a> <a id="plfa_plfa-part2-Confluence-18922" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">,</a> <a id="plfa_plfa-part2-Confluence-18924" href="../Confluence/#plfa_plfa-part2-Confluence-6833" class="Function">pars-betas</a> <a id="plfa_plfa-part2-Confluence-18935" href="../Confluence/#plfa_plfa-part2-Confluence-18881" class="Bound">M₂⇛N</a> <a id="plfa_plfa-part2-Confluence-18940" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">⟩</a> <a id="plfa_plfa-part2-Confluence-18942" href="../Confluence/#plfa_plfa-part2-Confluence-2197" class="InductiveConstructor Operator">⟩</a>
</pre><h2 id="notes">Notes</h2><p>This mechanized proof of confluence is based on several sources. The <code>subst-par</code> lemma is the “strong substitutivity” lemma of <span class="citation" data-cites="Schafer:2015">Schäfer, Tebbi, and Smolka (2015)</span>. The proofs of <code>par-triangle</code>, <code>strip</code>, and <code>par-confluence</code> are based on the notion of complete development by <span class="citation" data-cites="Takahashi:1995">Takahashi (1995)</span> and the technical report by <span class="citation" data-cites="Pfenning:1992">Pfenning (1992)</span> about the Church-Rosser theorem. In addition, we consulted Nipkow and Berghofer’s mechanization in Isabelle, which is based on an earlier paper by <span class="citation" data-cites="Nipkow:1996">Nipkow (1996)</span>.</p><h2 id="unicode">Unicode</h2><p>This chapter uses the following unicode:</p><pre><code>⇛ U+21DB RIGHTWARDS TRIPLE ARROW (\r== or \Rrightarrow)
⁺ U+207A SUPERSCRIPT PLUS SIGN (\^+)</code></pre><div id="refs" class="references csl-bib-body hanging-indent" role="list"><div id="ref-Nipkow:1996" class="csl-entry" role="listitem">Nipkow, Tobias. 1996. <span>“More Church-Rosser Proofs (in Isabelle/HOL).”</span> In <em>Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction</em>, 733–47. CADE-13. Berlin, Heidelberg: Springer-Verlag.</div><div id="ref-Pfenning:1992" class="csl-entry" role="listitem">Pfenning, Frank. 1992. <span>“A Proof of the Church-Rosser Theorem and Its Representation in a Logical Framework.”</span> CMU-CS-92-186. Carnegie Mellon University; Carnegie Mellon University.</div><div id="ref-Schafer:2015" class="csl-entry" role="listitem">Schäfer, Steven, Tobias Tebbi, and Gert Smolka. 2015. <span>“Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions.”</span> In <em>Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings 6</em>, 359–74. Springer.</div><div id="ref-Takahashi:1995" class="csl-entry" role="listitem">Takahashi, M. 1995. <span>“Parallel Reductions in λ-Calculus.”</span> <em>Information and Computation</em> 118 (1): 120–27. https://doi.org/<a href="https://doi.org/10.1006/inco.1995.1057">https://doi.org/10.1006/inco.1995.1057</a>.</div></div></div><nav class="pager"><ul class="pagination"><li><a class="pagelink" href="../Untyped/">Prev</a></li><li class="separator">•</li><li><a class="pagelink" href="https://github.com/plfa/plfa.github.io/blob/dev/src/plfa/part2/Confluence.lagda.md">Source</a></li><li class="separator">•</li><li><a class="pagelink" href="../BigStep/">Next</a></li><li class="separator">•</li></ul></nav></article></div></main><footer class="site-footer h-card"><data class="u-url" href="../"></data><div class="wrapper"><h2 class="footer-heading">Programming Language Foundations in Agda</h2><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Philip Wadler</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wadler" title="wadler"><i class="fab fa-github"></i>  wadler</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Wen Kokke</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wenkokke" title="wenkokke"><i class="fab fa-github"></i>  wenkokke</a></li><li><a rel="me" href="https://twitter.com/wenkokke" title="wenkokke"><i class="fab fa-twitter"></i>  wenkokke</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Jeremy G. Siek</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/jsiek" title="jsiek"><i class="fab fa-github"></i>  jsiek</a></li><li><a rel="me" href="https://twitter.com/jeremysiek" title="jeremysiek"><i class="fab fa-twitter"></i>  jeremysiek</a></li></ul></div><div class="footer-col footer-col-3"></div></div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a></div></footer></body></html>
⁺ U+207A SUPERSCRIPT PLUS SIGN (\^+)</code></pre><div id="refs" class="references csl-bib-body hanging-indent" data-entry-spacing="0" role="list"><div id="ref-Nipkow:1996" class="csl-entry" role="listitem">Nipkow, Tobias. 1996. <span>“More Church-Rosser Proofs (in Isabelle/HOL).”</span> In <em>Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction</em>, 733–47. CADE-13. Berlin, Heidelberg: Springer-Verlag.</div><div id="ref-Pfenning:1992" class="csl-entry" role="listitem">Pfenning, Frank. 1992. <span>“A Proof of the Church-Rosser Theorem and Its Representation in a Logical Framework.”</span> CMU-CS-92-186. Carnegie Mellon University; Carnegie Mellon University.</div><div id="ref-Schafer:2015" class="csl-entry" role="listitem">Schäfer, Steven, Tobias Tebbi, and Gert Smolka. 2015. <span>“Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions.”</span> In <em>Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings 6</em>, 359–74. Springer.</div><div id="ref-Takahashi:1995" class="csl-entry" role="listitem">Takahashi, M. 1995. <span>“Parallel Reductions in λ-Calculus.”</span> <em>Information and Computation</em> 118 (1): 120–27. https://doi.org/<a href="https://doi.org/10.1006/inco.1995.1057">https://doi.org/10.1006/inco.1995.1057</a>.</div></div></div><nav class="pager"><ul class="pagination"><li><a class="pagelink" href="../Untyped/">Prev</a></li><li class="separator">•</li><li><a class="pagelink" href="https://github.com/plfa/plfa.github.io/blob/dev/src/plfa/part2/Confluence.lagda.md">Source</a></li><li class="separator">•</li><li><a class="pagelink" href="../BigStep/">Next</a></li><li class="separator">•</li></ul></nav></article></div></main><footer class="site-footer h-card"><data class="u-url" href="../"></data><div class="wrapper"><h2 class="footer-heading">Programming Language Foundations in Agda</h2><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Philip Wadler</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wadler" title="wadler"><i class="fab fa-github"></i>  wadler</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Wen Kokke</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wenkokke" title="wenkokke"><i class="fab fa-github"></i>  wenkokke</a></li><li><a rel="me" href="https://twitter.com/wenkokke" title="wenkokke"><i class="fab fa-twitter"></i>  wenkokke</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Jeremy G. Siek</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/jsiek" title="jsiek"><i class="fab fa-github"></i>  jsiek</a></li><li><a rel="me" href="https://twitter.com/jeremysiek" title="jeremysiek"><i class="fab fa-twitter"></i>  jeremysiek</a></li></ul></div><div class="footer-col footer-col-3"></div></div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a></div></footer></body></html>
2 changes: 1 addition & 1 deletion Connectives/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -247,4 +247,4 @@
η U+03B7 GREEK SMALL LETTER ETA (\eta)
₁ U+2081 SUBSCRIPT ONE (\_1)
₂ U+2082 SUBSCRIPT TWO (\_2)
⇔ U+21D4 LEFT RIGHT DOUBLE ARROW (\&lt;=&gt;)</code></pre><aside id="footnotes" class="footnotes footnotes-end-of-document" role="doc-endnotes"><hr><ol><li id="fn1"><p>This paragraph was adopted from “Propositions as Types”, Philip Wadler, <em>Communications of the ACM</em>, December 2015.<a href="#fnref1" class="footnote-back" role="doc-backlink">↩︎</a></p></li></ol></aside></div><nav class="pager"><ul class="pagination"><li><a class="pagelink" href="../Isomorphism/">Prev</a></li><li class="separator">•</li><li><a class="pagelink" href="https://github.com/plfa/plfa.github.io/blob/dev/src/plfa/part1/Connectives.lagda.md">Source</a></li><li class="separator">•</li><li><a class="pagelink" href="../Negation/">Next</a></li><li class="separator">•</li></ul></nav></article></div></main><footer class="site-footer h-card"><data class="u-url" href="../"></data><div class="wrapper"><h2 class="footer-heading">Programming Language Foundations in Agda</h2><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Philip Wadler</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wadler" title="wadler"><i class="fab fa-github"></i>  wadler</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Wen Kokke</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wenkokke" title="wenkokke"><i class="fab fa-github"></i>  wenkokke</a></li><li><a rel="me" href="https://twitter.com/wenkokke" title="wenkokke"><i class="fab fa-twitter"></i>  wenkokke</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Jeremy G. Siek</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/jsiek" title="jsiek"><i class="fab fa-github"></i>  jsiek</a></li><li><a rel="me" href="https://twitter.com/jeremysiek" title="jeremysiek"><i class="fab fa-twitter"></i>  jeremysiek</a></li></ul></div><div class="footer-col footer-col-3"></div></div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a></div></footer></body></html>
⇔ U+21D4 LEFT RIGHT DOUBLE ARROW (\&lt;=&gt;)</code></pre><section id="footnotes" class="footnotes footnotes-end-of-document" role="doc-endnotes"><hr><ol><li id="fn1"><p>This paragraph was adopted from “Propositions as Types”, Philip Wadler, <em>Communications of the ACM</em>, December 2015.<a href="#fnref1" class="footnote-back" role="doc-backlink">↩︎</a></p></li></ol></section></div><nav class="pager"><ul class="pagination"><li><a class="pagelink" href="../Isomorphism/">Prev</a></li><li class="separator">•</li><li><a class="pagelink" href="https://github.com/plfa/plfa.github.io/blob/dev/src/plfa/part1/Connectives.lagda.md">Source</a></li><li class="separator">•</li><li><a class="pagelink" href="../Negation/">Next</a></li><li class="separator">•</li></ul></nav></article></div></main><footer class="site-footer h-card"><data class="u-url" href="../"></data><div class="wrapper"><h2 class="footer-heading">Programming Language Foundations in Agda</h2><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Philip Wadler</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wadler" title="wadler"><i class="fab fa-github"></i>  wadler</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Wen Kokke</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wenkokke" title="wenkokke"><i class="fab fa-github"></i>  wenkokke</a></li><li><a rel="me" href="https://twitter.com/wenkokke" title="wenkokke"><i class="fab fa-twitter"></i>  wenkokke</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Jeremy G. Siek</li><li><a class="u-email" href="mailto:[email protected]"><i class="far fa-envelope"></i>  [email protected]</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/jsiek" title="jsiek"><i class="fab fa-github"></i>  jsiek</a></li><li><a rel="me" href="https://twitter.com/jeremysiek" title="jeremysiek"><i class="fab fa-twitter"></i>  jeremysiek</a></li></ul></div><div class="footer-col footer-col-3"></div></div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a></div></footer></body></html>
Loading

0 comments on commit 2945ad0

Please sign in to comment.