Lecturas del año 2012

Lecturas de Enero de 2012

• L'ordinateur au cœur de la découverte mathématique.
• Últimos dos dígitos de (1+5^(2==n+1))/6. #Haskell ==
• Disparad contra la Ilustración.
• On the aesthetics of computer science.
• Computing with hereditarily finite sequences. #Prolog #MKM
• An interview with Stephen A. Cook
• Lecturas del Grupo de Lógica Computacional (Enero de 2012).
• Markov models. #Isabelle
• Turing machines por J. Hopcroft #Clásico #Divulgación
• The way forward for Computer Science in the U.K. #Enseñanza
• Teaching semantics with a proof assistant: No more LSD trip proofs. #Isabelle #Enseñanza
• Enseñando deducción natural con Coq. #Enseñanza #Lógica #Coq
• Formalisation en OWL pour vérifier les spécifications d’un environnement intelligent. #OWL
• Think complexity. #Sistemas_complejos #Python
• Algorithmic graph theory. #Libro #Sage
• A simplified framework for first-order languages and its formalization in Mizar. #Tesis #Metalógica #Mizar
• ProofPeer - A cloud-based interactive theorem proving system. #ProofPeer
• Generic proof tools and finite group theory. #Tesis #Coq

Lecturas de Febrero de 2012

• Lecturas del Grupo de Lógica Computacional (Enero de 2012).
• Emergence and refinement. #Sistemas_complejos
• Formalizing a hierarchical file system. #PVS
• Etude et formalisation de la méthode de Wu dans Coq. #Tesis #Coq
• Using PVS to investigate incidents through the lens of distributed cognition. #PVS
• Formal system verification for trustworthy embedded systems. #Isabelle
• The mechanical verification of a DPLL-based satisfiability solver. #PVS
• Innovación en el tratamiento de la información desde la Ingeniería del Conocimiento (1/2)
• Innovación en el tratamiento de la información desde la Ingeniería del Conocimiento (2/2)
• A unified treatment of syntax with binders.
• The age of Big Data. #IA
• Crear moléculas desde cero sin la endiablada ecuación de Schrödinger. #IA
• Refinement for monadic programs. #Isabelle
• Dijkstra's shortest path algorithm. #Isabelle
• Computational topology.
• Category theory and functional programming. #Haskell
• The artist in the computer scientist: more humanity to our research.
• When formal systems kill: computer ethics and formal methods.
• Mathematics in the age of the Turing machine. #Panorama #DAO
• The reflective Milawa theorem prover is sound. #ACL2 #HOL4
• Ejercicios de "Informática de 1º de Matemáticas" (2011-12). #Haskell
• Temas de programación funcional con Haskell (curso 2011-12). #Haskell
• Executable transitive closures. #Isabelle

Lecturas de Marzo de 2012

• Automatic proofs and refutations for higher-order logic. #Tesis #Isabelle
• On theorem prover-based testing. #Isabelle
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. #Coq
• Tips on Haskell. #Tutorial #Haskell
• Enfragmo: A system for modelling and solving search problems with logic. #SAT
• Logic & reasoning: from Aristotle to Intel. #Panorama #Lógica
• Deciding Kleene Algebras in Coq. #Coq
• Vérification semi-automatique de primitives cryptographiques. #Tesis #Coq
• Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model. #PVS
• Formal error analysis and verification of the frequency domain equalizer. #HOL
• Introduction to the Coq proof-assistant for practical software verification. #Tutorial #Coq
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination #Coq
• Mathematics for Computer Science. #Libro
• Proving possibilistic, probabilistic noninterference. #Isabelle
• Decision procedures in Algebra and Logic (Reading material). #Libro #Lógica
• A formalization of the theorem of existence of first-order most general unifiers. #PVS

Lecturas de Abril de 2012

• The worldʼs shortest correct exact real arithmetic program?. #PVS #Haskell
• Kleene algebra, rewriting modulo AC and circuits in Coq. #Tesis #Coq
• Deriving a fast inverse of the generalized Cantor n-tupling bijection. #Prolog
• PVS linear algebra libraries for verification of control software algorithms in C/ACSL. #PVS
• Generating verifiable Java code from verified PVS specifications. #PVS
• Haskell gets argumentative. #Haskell #Lógica @IA
• Induction and recursion. #Fundamentos
• A formal proof of Sasaki-Murao algorithm. #Coq
• Essential incompleteness of arithmetic verified by Coq. #Coq
• Incompleteness & completeness: Formalizing logic and analysis in type theory. #Tesis #Coq
• Well-quasi-orders. #Isabelle
• Analyse et Conception Formelles (Software formal analysis and design). #Curso #Isabelle

Lecturas de Mayo de 2012

• Programming and proving in Isabelle/HOL. #Isabelle
• Numerical analysis of ordinary differential equations. #Isabelle
• Inductive study of confidentiality. #AFP #Isabelle
• Formal correctness of security protocols. #Libro #Isabelle
• Stuttering equivalence. #AFP
• HaskHOL: A Haskell hosted domain specific language for Higher-Order Logic theorem proving. #Tesis #Haskell
• A string of pearls: proofs of Fermat's little theorem. #HOL4
• Separation logic: A logic for shared mutable data structures.
• Local action and abstract separation logic.
• Separation algebra. #Isabelle
• Using PVS to support the analysis of distributed cognition systems. #PVS
• Formal verification of the heavy hitter problem. #HOL
• Formal probabilistic analysis using theorem proving. #Tesis #HOL
• Proving equational Haskell properties using automated theorem provers. #Haskell #Thesis
• Accessible integrated formal reasoning environments in classroom instruction of mathematics.
• Designing accessible lightweight formal verification systems.
• Artificial intelligence: from fantasy to reality. #IA
• HipSpec: Automating inductive proofs of program properties. #Haskell
• Supplementary material for "Thinking as computation". #IA #Prolog
• Verifying an algorithm computing discrete vector fields for digital imaging. #Coq
• Bridging the gap: Automatic verified abstraction of C
• Computing in Cantor’s paradise with λZFC.
• Thoughts on gamifying textbooks.
• Isabelle/Circus: A process specification and verification environment. #Isabelle
• Isabelle/Circus. #Isabelle
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program #Coq

Lecturas de Junio de 2012

• Large-scale formal verification in practice: A process perspective. #Isabelle
• A framework for formally verifying software transactional memory algorithms. #PVS
• Rigorous polynomial approximation using Taylor models in Coq. #Coq
• Rigorous polynomial approximations and applications. #Tesis #Coq

Lecturas de Julio de 2012

• Seventy four minutes of mathematics: An analysis of the third Mini-Polymath project. #MKM
• Formalizing Kruskal’s tree theorem in Isabelle/HOL. #Isabelle
• Verifying an algorithm computing discrete vector fields for digital imaging. #Coq
• Formal verification of monad transformers. #Isabelle
• HALO: Haskell to logic through denotational semantics. #Haskell
• Interactive proof: Introduction to Isabelle/HOL. #Tutorial #Isabelle
• Formalization of an efficient representation of Bernstein polynomials and applications to global optimization #PVS
• Lifting and transfer: A modular design for quotients in Isabelle/HOL. #Isabelle
• Meta-theory à la carte. #Coq
• Mechanization of an algorithm for deciding KAT terms equivalence. #Coq
• ¿Es posible construir software que no falle?. #Verificación

Lecturas de Agosto de 2012

• Proving the impossibility of trisecting an angle and doubling the cube. #Isabelle
• Formal specification and verification of well-formedness in business process product lines. #PVS
• Compiling concurrency correctly (Verifying software transactional memory). #Tesis #Agda #Haskell
• Représentation coinductive des graphes. #Tesis #Coq
• Formalizing adequacy: A case study for higher-order abstract syntax. #Isabelle
• Algorithms in games evolving in time: Winning strategies based on testing. #Isabelle
• A certified JavaScript interpreter. #Coq
• Formalization of Shannon’s theorems in SSReflect-Coq. #Coq
• Abstract interpretation of annotated commands. #Isabelle
• Construction of real algebraic numbers in Coq. #Coq
• Correctness of pointer manipulating algorithms illustrated by a verified BDD construction. #Isabelle
• Towards provably robust watermarking. #Coq
• Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL. #Isabelle
• Formalizing an abstract algebra textbook in Isabelle/HOL. #Isabelle
• Numerical analysis of ordinary differential equations in Isabelle/HOL. #Isabelle
• A refinement-based approach to computational algebra in Coq. #Coq
• Coherent and strongly discrete rings in type theory. #Coq
• Logic * control: An example of program construction. #Prolog
• Deriving a fast inverse of the generalized Cantor N-tupling bijection. #Prolog
• Formalization and verification of number theoretic algorithms using the Mizar proof checker. #Mizar

Lecturas de Septiembre de 2012

• Operational refinement for compiler correctness. #Tesis #Coq
• Interactive and automated proofs for graph transformations. #Isabelle
• Lecturas del Grupo de Lógica Computacional (Marzo-Agosto de 2012)
• Piensa en Haskell (Ejercicios de programación funcional con Haskell). #Haskell
• ¿Computadores von Neumann, o computadores Turing? #Historia
• Formalizing Frankl's conjecture: FC-families. #Isabelle
• Implementing an efficient theorem prover. #Tesis #Vampire
• System of logic based on ordinals. #Tesis #Historia
• Proving concurrent noninterference (código) #Isabelle
• Improving real analysis in Coq: a user-friendly approach to integrals and derivatives. #Coq (CPP2012)
• Computing persistent homology within Coq/SSReflect. #Coq
• Software libre para una sociedad libre. #Libro #Pensamiento
• A formal proof of Sasaki-Murao algorithm. #Coq (MAP2012, code, Presentación).

Lecturas de Octubre de 2012

• Confluence by decreasing diagrams formalized. #Isabelle
• Proof Pearl – A mechanized proof of GHC’s mergesort. #Isabelle #Haskell
• A logic-algebraic approach to decision taking in a railway interlocking system. #BG
• Scheme in industrial automation. #Scheme
• Parallelizing an interactive theorem prover: Functional programming and proofs with ACL2. #ACL2 #Tesis
• A string of pearls: Proofs of Fermat’s little theorem. #HOL4
• A formally-verified C compiler supporting floating-point arithmetic. #Coq
• The Boyer-Moore waterfall model revisited. #HOL_Light
• A Python pattern matcher project for an introduction to Artificial Intelligence course. #IA

Lecturas de Noviembre de 2012

• Informatik 2: Functional programming. #Haskell
• Contributions to the formal verification of arithmetic algorithms. #Tesis #Coq
• Why learn Haskell?. #Tutorial #Haskell
• A mechanical verification of the independence of Tarski's euclidean axiom y código #Tesina #Isabelle
• Weak completeness theorem for propositional linear time temporal logic. #Mizar
• Natural language processing for the working programmer. #Haskell #IA
• Nexus authorization logic (NAL): Logical results. #Coq
• Reasons for studying Haskell in University. #Haskell
• Constructive completeness for modal logic with transitive closure. #Coq #Modal
• A functional programming approach to AI search algorithms. #IA #PF
• Dual multi-adjoint concept lattices. #AFC
• Temas de "Demostración asistida por ordenador". #Isabelle #Tutorial
• Verificación de programas: Introducción. #Verificación
• Último dígito del producto de números de Fermat. #Haskell #IMO
• A formal proof of square root and division elimination in embedded programs. #PVS
• Coq et caractères (Preuve formelle du théorème de Feit et Thompson). #Coq #Divulgación
• Formalized algebraic numbers: construction and first order theory. #Tesis #Coq
• How enterprises use functional languages, and why they don't. #PF
• Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting. #Tesis #Isabelle
• Constructive formalization of regular languages. #Tesina #Coq
• Computing with free algebras. #Haskell
• Ask-Elle: a Haskell Tutor. #Tesis #Haskell #TI
• Using Isabelle to verify special relativity, with application to hypercomputation theory. #Isabelle

Lecturas de Diciembre de 2012

• Lecturas del Grupo de Lógica Computacional (Septiembre-Noviembre de 2012).
• Verifying probabilistic correctness in Isabelle with pGCL. #Isabelle
• Formalization of a strategy for the KRK chess endgame. #Coq
• Formalization and implementation of algebraic methods in Geometry. #Isabelle
• Formal verification of conflict detection algorithms for arbitrary trajectories. #PVS
• Learning-assisted automated reasoning with Flyspeck. #Mizar
• Deductive formal verification of embedded systems. #Tesis #Coq
• Verification of redecoration for infinite triangular matrices using coinduction. #Coq
• Représentation coinductive des graphes. #Tesis #Coq
• Formal mathematics for mathematicians.
• The HOL Light theory of euclidean space. #HOL_Light
• Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar. #Mizar
• The Gödel completeness theorem for uncountable languages. #Mizar
• Machine learning in Proof General: Interfacing interfaces. #Coq
• Interactive verification of Markov chains: Two distributed protocol case studies. #Isabelle
• Du rêve à la réalité des preuves. (Interstices, 2012) #Divulgación #DAO
• Interactive theorem proving, automated reasoning, and mathematical computation