Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] In the AFP: Decreasing Diagrams II

view this post on Zulip Email Gateway (Aug 22 2022 at 10:56):

From: Larry Paulson <lp15@cam.ac.uk>
AFP entries seem to be pouring in! The latest is now available at

http://afp.sourceforge.net/entries/Decreasing-Diagrams-II.shtml

Larry Paulson

Decreasing Diagrams II
Bertram Felgenhauer

abstract:
This theory formalizes the commutation version of decreasing diagrams
for Church-Rosser modulo. The proof follows Felgenhauer and van Oostrom
(RTA 2013). The theory also provides important specializations, in
particular van Oostrom’s conversion version (TCS 2008) of decreasing
diagrams.

Last updated: Apr 26 2024 at 20:16 UTC