[isabelle] AFP 2021

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.


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.


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.


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


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.


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.


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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.