Lecturas del Grupo de Lógica Computacional (Marzo-Agosto de 2012)
Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el mes de marzo de 2012. La anterior recopilación fue la de febrero de 2012.
La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.
- 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
- 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
- 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
- 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
- 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
- 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
En Mendeley también se encuentran las lecturas del Grupo de Lógica Computacional.