He publicado una ampliación del libro Exámenes de programación funcional con Haskell (2009-2014). El libro es una recopilación de los exámenes de la asignatura de Informática (de primero del Grado en Matemáticas) desde el curso 2009-10 hasta el actual.
Tras la ampliación, el libro contiene 102 exámenes y 648 ejercicios.
Este libro es el complemento de los anteriores:
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Real-valued special functions: upper and lower bounds
Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).
Su resumen es
This development proves upper and lower bounds for several familiar real-valued functions. For sin, cos, exp and sqrt, it defines and verifies infinite families of upper and lower bounds, mostly based on Taylor series expansions. For arctan, ln and exp, it verifies a finite collection of upper and lower bounds, originally obtained from the functions’ continued fraction expansions using the computer algebra system Maple. A common theme in these proofs is to take the difference between a function and its approximation, which should be zero at one point, and then consider the sign of the derivative. The immediate purpose of this development is to verify axioms used by MetiTarski, an automatic theorem prover for real-valued special functions. Crucial to MetiTarski’s operation is the provision of upper and lower bounds for each function of interest.
El trabajo se ha publicado en en AFP (The Archive of Formal Proofs).
El código de las correspondientes teorías se encuentra aquí.
Se ha publicado un artículo de razonamiento formalizado en Coq titulado [Combining proofs and programs in a dependently typed language](
Sus autores son Chris Casinghino, Vilhelm Sjöberg y Stephanie Weirich (de la Universidad de Pensilvania, EE.UU.).
Su resumen es
Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, Ωmega. Here, we combine these two approaches into a single dependently-typed core language. The language is composed of two fragments that share a common syntax and overlapping semantics: a logic that guarantees total correctness, and a call-by-value programming language that guarantees type safety but not termination. The two fragments may interact: logical expressions may be used as programs; the logic may soundly reason about potentially nonterminating programs; programs can require logical proofs as arguments; and “mobile” program values, including proofs computed at runtime, may be used as evidence by the logic. This language allows programmers to work with total and partial functions uniformly, providing a smooth path from functional programming to dependently-typed programming.
El trabajo se presentó en el POPL 2014 (41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages).
El código de las correspondientes teorías en … se encuentra aquí.
Se ha publicado un artículo de razonamiento formalizado en Coq titulado Mechanized network origin and path authenticity proofs.
Sus autores son Fuyuan Zhang, Limin Jia, Cristina Basescu, Tiffany Hyun-Jin Kim, Yih-Chun Hu y Adrian Perrig.
Su resumen es
A secure routing infrastructure is vital for secure and reliable Internet services. Source authentication and path validation are two fundamental primitives for building a more secure and reliable Internet. Although several protocols have been proposed to implement these primitives, they have not been formally analyzed for their security guarantees. In this paper, we apply proof techniques for verifying cryptographic protocols (e.g., key exchange protocols) to analyzing network protocols. We encode LS 2, a program logic for reasoning about programs that execute in an adversarial environment, in Coq. We also encode protocol-specific data structures, predicates, and axioms. To analyze a source-routing protocol that uses chained MACs to provide origin and path validation, we construct Coq proofs to show that the protocol satisfies its desired properties. To the best of our knowledge, we are the first to formalize origin and path authenticity properties, and mechanize proofs that chained MACs can provide the desired authenticity properties.
El trabajo se presentará en el ACM CCS 2014 (21st ACM Conference on Computer and Communications Security).
El código de las correspondientes teorías en Coq se encuentra aquí.
El curso Lógica informática (de 2º de Grado en Ingeniería Informática) comienza el lunes 22 de septiembre.
Las clases son los lunes de 10:30 a 12:30 y los miércoles de 12:30 a 14:30 en el aula I1.10 de la ETSII.
La página con los materiales del curso se encuentra aquí.