Email Gateway (Feb 23 2021 at 10:19): Email Gateway (Feb 23 2021 at 10:19):From: Gerwin Klein <kleing@unsw.edu.au>
The AFP is now available for Isabelle2021 from https://isa-afp.org
There are now more than 2.8 million lines of Isabelle proof in 582 entries by 374 authors.
The following entries that were previously in the development version are now available from the front page.
Enjoy!
Gerwin
A Formalization of Web Components
=================================
by Achim D. Brucker and Michael Herzberg
While the DOM with shadow trees provide the technical basis for defining web components, the DOM standard neither defines the concept of web components nor specifies the safety properties that web components should guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying the DOM respect component boundaries. In AFP entry, we present a formally verified model of web components and define safety properties which ensure that different web components can only interact with each other using well-defined interfaces. Moreover, our verification of the application programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM API need to preserve to ensure the integrity of components.
https://www.isa-afp.org/entries/DOM_Components.html
Hood-Melville Queue
===================
by Alejandro Gómez-Londoño
This is a verified implementation of a constant time queue. The original design is due to Hood and Melville. This formalization follows the presentation in Purely Functional Data Structuresby Okasaki.
https://www.isa-afp.org/entries/Hood_Melville_Queue.html
Inline Caching and Unboxing Optimization for Interpreters
=========================================================
by Martin Desharnais
This Isabelle/HOL formalization builds on the VeriComp entry of the Archive of Formal Proofs to provide the following contributions:
• an operational semantics for a realistic virtual machine (Std) for dynamically typed programming languages;
• the formalization of an inline caching optimization (Inca), a proof of bisimulation with (Std), and a compilation function;
• the formalization of an unboxing optimization (Ubx), a proof of bisimulation with (Inca), and a simple compilation function.
This formalization was described in the CPP 2021 paper Towards Efficient and Verified Virtual Machines for Dynamic Languages
https://www.isa-afp.org/entries/Interpreter_Optimizations.html
A Formalization of Knuth–Bendix Orders
======================================
by Christian Sternagel
We define a generalized version of Knuth–Bendix orders, including subterm coefficient functions. For these orders we formalize several properties such as strong normalization, the subterm property, closure properties under substitutions and contexts, as well as ground totality.
https://www.isa-afp.org/entries/Knuth_Bendix_Order.html
Extensions to the Comprehensive Framework for Saturation Theorem Proving
========================================================================
by Jasmin Blanchette and Sophie Tourret
This Isabelle/HOL formalization extends the AFP entry Saturation_Framework with the following contributions:
• an application of the framework to prove Bachmair and Ganzinger's resolution prover RP refutationally complete, which was formalized in a more ad hoc fashion by Schlichtkrull et al. in the AFP entry Ordered_Resultion_Prover;
• generalizations of various basic concepts formalized by Schlichtkrull et al., which were needed to verify RP and could be useful to formalize other calculi, such as superposition;
• alternative proofs of fairness (and hence saturation and ultimately refutational completeness) for the given clause procedures GC and LGC, based on invariance.
https://www.isa-afp.org/entries/Saturation_Framework_Extensions.html
A Formal Model of the Document Object Model with Shadow Roots
=============================================================
by Achim D. Brucker and Michael Herzberg
In this AFP entry, we extend our formalization of the core DOM with Shadow Roots. Shadow roots are a recent proposal of the web community to support a component-based development approach for client-side web applications. Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be backward compatible, such extensions often result in complex specification that may contain unwanted subtleties that can be detected by a formalization. Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can be extended without the need of re-proving already proven properties and executable, i.e., we can generate executable code from our specification. We exploit the executability to show that our formalization complies to the official standard of the W3C, respectively, the WHATWG.
https://www.isa-afp.org/entries/Shadow_DOM.html
Email Gateway (Feb 23 2021 at 11:56):From: Makarius <makarius@sketis.net>
Great. It looks like healthy and sustainable growth, although the
"lines-of-code" count might be a bit crude as a measure:
https://www.isa-afp.org/statistics.html
I will continue to do my best in scaling the underlying Isabelle
infrastructure further (together with David Matthews for Poly/ML).
Overall, we have made huge progress in the past 15 years.
Makarius
Last updated: Jul 15 2022 at 23:21 UTC