Email Gateway (Jun 03 2024 at 16:26): Email Gateway (Jun 03 2024 at 16:26):From: Tobias Nipkow <nipkow@in.tum.de>
Verifying a Decision Procedure for Pattern Completeness
René Thiemann and Akihisa Yamada
Pattern completeness is the property that the left-hand sides of a functional
program or term rewrite system cover all cases w.r.t. pattern matching. We
verify a recent (abstract) decision procedure for pattern completeness that
covers the general case, i.e., in particular without the usual restriction of
left-linearity. In two refinement steps, we further develop an executable
version of that abstract algorithm. On our example suite, this verified
implementation is faster than other implementations that are based on
alternative (unverified) approaches, including the complement algorithm, tree
automata encodings, and even the pattern completeness check of the GHC Haskell
compiler.
https://www.isa-afp.org/entries/Pattern_Completeness.html
Sorted Terms
Akihisa Yamada and René Thiemann
This entry provides a basic library for many-sorted terms and algebras. We view
sorted sets just as partial maps from elements to sorts, and define sorted set
of terms reusing the data type from the existing library of (unsorted) first
order terms. All the existing functionality, such as substitutions and contexts,
can be reused without any modifications. We provide predicates stating what
substitutions or contexts are considered sorted, and prove facts that they
preserve sorts as expected.
https://www.isa-afp.org/entries/Sorted_Terms.html
Enjoy!
Last updated: Oct 31 2025 at 08:28 UTC