Lecturas del año 2012
Revisión del 18:42 27 abr 2013 de Jalonso (discusión | contribuciones)
Sumario
- 1 Lecturas de Enero de 2012
- 2 Lecturas de Febrero de 2012
- 3 Lecturas de Marzo de 2012
- 4 Lecturas de Abril de 2012
- 5 Lecturas de Mayo de 2012
- 6 Lecturas de Junio de 2012
- 7 Lecturas de Julio de 2012
- 8 Lecturas de Agosto de 2012
- 9 Lecturas de Septiembre de 2012
- 10 Lecturas de Octubre de 2012
- 11 Lecturas de Noviembre de 2012
- 12 Lecturas de Diciembre de 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 #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