Term rewriting and applications

Más información sobre el libro

This work covers a range of topics in formal verification and rewriting systems, beginning with the challenges in optimizing compilers and satisfiability modulo theories. It explores logical foundations for explicit substitutions and examines the role of intruders in security contexts. The application of rewriting in Java is discussed, alongside the development of approximations for static analyzers and the determination of unify-stable presentations. The confluence of pattern-based calculi is addressed, along with a proof that super-consistency implies cut elimination. The text delves into bottom-up rewriting and its preservation of inverse recognizability, as well as adjunction methods for garbage collection in graph rewriting. Key concepts include non-strict confluent rewrite systems, symbolic model checking of infinite-state systems, and the decidability of innermost-reachability and innermost-joinability for shallow term rewrite systems. The work also tackles termination of rewriting with right-flat rules and the completeness of context-sensitive order-sorted specifications. Applications of rewriting logic to language prototyping and analysis are highlighted, along with proofs related to strong normalization for explicit substitution calculi. Additional topics include sequence unification, correctness in calculi with letrec, and characterizations of rewriting rules. The maximum length of mu-reduction in lambda mu-calculu