I1M2013: Funciones de orden superior en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se han estudiado las funciones de orden superior y las funciones de procesamiento de listas (map y filter).

Además, se ha estudiado cómo puede abstraerse los esquemas definición de funciones de recursión sobre listas mediante la función de plegado (foldr) y cómo con dicha función puede simplificarse la definición de funciones.

A continuación se ha visto cómo definir funciones con acumuladores y cómo simplificarlas con el patrón de plegado por la izquierda (foldl).

Finalmente, se ha visto cómo puede simplificarse la definición de funciones usando el operador de composición.

Las transparencias usadas en la clase son las páginas 1 a 23 del tema 7
Read More “I1M2013: Funciones de orden superior en Haskell”

Using Isabelle/HOL to verify first-order relativity theory

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre la teoría de la relatividad titulado Using Isabelle/HOL to verify first-order relativity theory.

Sus autores son

Su resumen es

Logicians at the Rényi Mathematical Institute in Budapest have spent several years developing versions of relativity theory (special, general, and other variants) based wholly on first-order logic, and have argued in favour of the physical decidability, via exploitation of cosmological phenomena, of formally unsolvable questions such as the Halting Problem and the consistency of set theory. As part of a joint project, researchers at Sheffield have recently started generating rigorous machine-verified versions of the Hungarian proofs, so as to demonstrate the sound- ness of their work. In this paper, we explain the background to the project and demonstrate a first-order proof in Isabelle/HOL of the theorem “no inertial observer can travel faster than light”. This approach to physical theories and physical computability has several pay-offs, because the precision with which physical theories need to be formalised within automated proof systems forces us to recognise subtly hidden assumptions.

El código de las correspondientes teorías en Isabelle se encuentra aquí.

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.

Concrete semantics (A proof assistant approach)

PorJosé A. Alonso

Se ha publicado un libro de razonamiento formalizado en Isabelle/HOL sobre semántica de lenguajes de programación titulado Concrete semantics (A proof assistant approach).

Sus autores son

Su resumen es

The book Concrete Semantics introduces semantics of programming languages through the medium of a proof assistant. The first part of the book is an introduction to the proof assistant Isabelle. The second part is an introduction to operational semantics and its applications and is based on a simple imperative programming language.

El código de las correspondientes teorías en Isabelle se encuentra aquí.