Email Gateway (Aug 22 2022 at 15:25): Email Gateway (Aug 22 2022 at 15:25):From: Lawrence Paulson <lp15@cam.ac.uk>
We have a new entry courtesy of Steven Obua:
This formalisation accompanies the paper Local Lexing which introduces a novel parsing concept of the same name. The paper also gives a high-level algorithm for local lexing as an extension of Earley's algorithm. This formalisation proves the algorithm to be correct with respect to its local lexing semantics. As a special case, this formalisation thus also contains a proof of the correctness of Earley's algorithm. The paper contains a short outline of how this formalisation is organised.
You will find it online here: https://www.isa-afp.org/entries/LocalLexing.shtml
That is five entries for April!
Larry Paulson
Email Gateway (Aug 22 2022 at 18:42):From: Lawrence Paulson <lp15@cam.ac.uk>
We have a new contribution, thanks to David Fuenmayor and Christoph Benzmüller:
The proof document is a full paper describing the work.
This is one of a number of entries concerned with the formalisation of philosophical theories. We have a new topic, Logic/Philosophy, and I've taken the liberty of moving some existing entries to this topic. These include a number of proofs of the existence of God.
The new entry is at https://www.isa-afp.org/entries/GewirthPGCProof.html.
Larry Paulson
Email Gateway (Aug 22 2022 at 20:45):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce yet another new entry. You'll find it online at
https://www.isa-afp.org/entries/Clean.html
Clean - An Abstract Imperative Programming Language and its Theory
Frédéric Tuong and Burkhart Wolff
Clean is based on a simple, abstract execution model for an imperative target language. “Abstract” is understood in contrast to “Concrete Semantics”; alternatively, the term “shallow-style embedding” could be used. It strives for a type-safe notion of program-variables, an incremental construction of the typed state-space, support of incremental verification, and open-world extensibility of new type definitions being intertwined with the program definitions. Clean is based on a “no-frills” state-exception monad with the usual definitions of bind and unit for the compositional glue of state-based computations. Clean offers conditionals and loops supporting C-like control-flow operators such as break and return. The state-space construction is based on the extensible record package. Direct recursion of procedures is supported. Clean’s design strives for extreme simplicity. It is geared towards symbolic execution and proven correct verification tools. The underlying libraries of this package, however, deliberately restrict themselves to the most elementary infrastructure for these tasks. The package is intended to serve as demonstrator semantic backend for Isabelle/C, or for the test-generation techniques.
Larry
Last updated: Apr 23 2024 at 12:29 UTC