First-order logic completeness for the lazy programmer

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado First-order logic completeness for the lazy programmer.

Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Universidad Técnica de Munich, Alemania).

Su resumen es

Codatatypes are regrettably absent from many programming languages and proof assistants. We make a case for their usefulness by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. Codatatypes help capture the essence of the proof, which establishes an abstract property of derivation trees independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation, especially for readers acquainted with lazy data structures. The proof is formalized in Isabelle/HOL and demonstrates the recently introduced definitional package for codatatypes and its integration with Isabelle’s Haskell code generator.

Applications of interactive proof to data flow analysis and security

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre semántica de lenguajes de programación titulado Applications of interactive proof to data flow analysis and security.

Sus autores son

Su resumen es

We show how to formalise a small imperative programming language in the theorem prover Isabelle/HOL, how to define its semantics, and how to prove properties about the language, its type systems, and a number of data flow analyses.

The emphasis is not on formalising a complex language deeply, but to teach a number of formalisation techniques and proof strategies using simple examples. For this purpose, we cover a basic type system with type safety proof, more complex security type systems, also with soundness proofs, and different kinds of data flow analyses, in particular definite initialisation analysis and constant propagation, again with correctness proofs.