Lecturas del año 2011
Revisión del 06:16 28 abr 2013 de Jalonso (discusión | contribuciones)
Sumario
- 1 Lecturas de Enero de 2011
- 2 Lecturas de Febrero de 2011
- 3 Lecturas de Marzo de 2011
- 4 Lecturas de Abril de 2011
- 5 Lecturas de Mayo de 2011
- 6 Lecturas de Junio de 2011
- 7 Lecturas de Julio de 2011
- 8 Lecturas de Agosto de 2011
- 9 Lecturas de Septiembre de 2011
- 10 Lecturas de Octubre de 2011
- 11 Lecturas de Noviembre de 2011
- 12 Lecturas de Diciembre de 2011
Lecturas de Enero de 2011
- Semantic web reasoners and languages #RA #WS
- El 2011 y los números primos (en Haskell) #Haskell
- The dialectica interpertation in Coq #Coq
- Errores aritméticos en Haskell y en Lisp #Haskell #Lisp
- Why Lisp is a big hack (and Haskell is doomed to succeed) #Lisp #Haskell
- ProofWiki y la verificación de las demostraciones matemáticas #Verificación #MKM
- A quick and gentle guide to constraint logic programming via ECLiPSe #PL #Restricciones
- A language for mathematical knowledge management #MKM
- Automated inference of finite unsatisfiability #AR
- The free vector space on a type. #Haskell
- Formal methods applied to a floating-point number system #Z
- A machine-checked theory of floating point arithmetic #HOL_Light
- Formal verification of floating point trigonometric functions #HOL_Light
- A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon TM processor #ACL2
- A generic library for floating-point numbers and its application to exact computing #Coq.
- A high-level formalization of floating-point numbers in PVS #PVS
- Formal verification of floating-point programs #Coq
- The pitfalls of verifying floating-point computations #Verificación
- Floats and ropes: A case study for formal numerical program verification #Coq.
- Formal reliability analysis of combinational circuits using theorem proving #HOL
- Programación funcional con Haskell #Libro #Haskell
- Certifying compilers using higher-order theorem provers as certificate checker #Isabelle #Coq
- El tipo abstracto de datos de las colas en Haskell #Haskell
Lecturas de Febrero de 2011
- Deducción natural en lógica proposicional con Isabelle/Isar #Isabelle
- Deducción natural en lógica de primer orden con Isabelle/Isar #Isabelle
- A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL. #Isabelle
- El tipo abstracto de datos de las colas de prioridad en Haskell #Haskell
- Program verification and functioning of operative computing revisited: How about mathematics engineering? #Verificación
- El próximo después de 1811 #Haskell
- Charming proofs: A journey into elegant mathematics #Libro #DAO
- Functional binomial queues #RF #Isabelle
- Lower semicontinuous functions #RF #Isabelle
- Lógica Informática (2010-11) #LI
- Artificial intelligence (Foundations of computational agents) #Libro #IA
Lecturas de Marzo de 2011
- Software verification turns maintstream #Verificación
- Formalising, improving, and reusing the Java module system http://bit.ly/dF68vF #Tesis #Isabelle
- SMT solvers: new oracles for the HOL theorem prover #SMT #HOL4
- Isabelle como un lenguaje funcional #Isabelle
- El tipo abstracto de datos de las pilas en Haskell #Haskell
- El tipo abstracto de datos de las colas en Haskell #Haskell
- Executable transitive closures of finite relations #RF #Isabelle
+ Reduced ordered binary decision diagram with implied literals: A new knowledge compilation approach #AR
- Introduction to artificial intelligence #Libro #IA
- Experience report: Functional programming through deep time (Modeling the first complex ecosystems on Earth) #Haskell
- Logic-based artificial intelligence #Libro #IA
- A Formalization of the C99 Standard in HOL, Isabelle and Coq #HOL #Isabelle #Coq
- Formal methods in agent-oriented software engineering #MF
- The cognitive agents specification language and verification environment #Verificación
- Software bugs and scientific progress #Verificación
- Representing model theory in a type-theoretical logical framework #RF #Twelfe
- Towards a verification framework for faulty message passing systems in PVS #PVS
Lecturas de Abril de 2011
- Por qué y cómo se hace investigación en matemáticas #CM
- Introduction to newLISP #Libro #Lisp
- Verified firewall policy transformations for test case generation #Isabelle
- An approach to modular and testable security models of real-world health-care applications #Isabelle
- Psi-calculi: a framework for mobile processes with nominal data and logic #Isabelle
- Simplification rules for intuitionistic propositional tableaux #AR
- A fast and verified algorithm for proving store-and-forward networks deadlock-free #ACL2
- Gestión mecanizada del conocimiento matemático en Topología algebraica #Tesis #ACL2
- The first formalized math wiki is here #MKM
- Extending Sledgehammer with SMT Solvers #Isabelle #SMT
- Book of proof #Libro #DAO
- The general triangle is unique #RF #Isabelle
- NASA Formal Methods #Libro #MF #Verificación
- Haskell for the cloud #Haskell
- The opentheory standard theory library #Verificación
- A Coq-based library for interactive and automated theorem proving in plane geometry #RF #Coq
- Mechanical support for efficient dissemination on the CAN overlay network #Isabelle
- A Wiki for formal mathematics #MKM
- Recent developments in computing and philosophy #Prover9
- Constructive formalization of classical modal logic. #Coq
- Proving equality between streams #Coq
- The limits of correctness #Verificación
- A formal proof of the Riesz representation theorem #RF #PVS
- A formal proof that π₁(S¹)=Z #RF #Coq
Lecturas de Mayo de 2011
- Balancing weight-balanced trees #Coq #Haskell
- A formal programming model of Orléans skeleton library #Coq
- Formal verification of a small real-time operating system #Tesis #Isabelle
- Deus ex machina. #Prover9
- Computationally-discovered simplification of the ontological argument. #Prover9
- Satisfiability of acyclic and almost acyclic CNF formulas (II) #AR
- Heaps and data structures: A challenge for automated provers #AR
- Haskell: Not pure enough? #Haskell
- Verified stack-based genetic programming via dependent types #RF #Agda #IA
- Sorpresa sumando potencias de 2 en Haskell #Haskell
- A list-machine benchmark for mechanized metatheory #AR
- The locally nameless representation #AR
- Formalização da prova do teorema de existência de unificadores mais gerais em teorias de primeira-ordem #TFM #PVS
- Solving Rubik's cube using SAT solvers #SAT
- Programação funcional: Novos horizontes para a expansão da consciência #PF
- Computer certified efficient exact reals in Coq #Coq
- Parallel and concurrent programming in Haskell #Haskell
- TRX: A formally verified parser interpreter #Coq
- Computational meta-ethics: Towards the meta-ethical robot #Prover9
- Formal metatheory of programming languages in the Matita interactive theorem prover #RF #Matita
- ALPprolog — A new logic programming method for dynamic domains #PL
- Logical formalization of semantic business vocabulary and Rules #RC
- The proof is in the pudding (The changing nature of mathematical proof) #Libro #LI
- Knowledge-based programs #RF #Isabelle
- Elegance and power #Haskell
- Validated compilation through logic #Verificación
- Teaching computational logic: Technology-enhanced learning and animations #Enseñanza #LI
- Sigma: An integrated development environment for formal ontology #RC
- Termination of Isabelle functions via termination of rewriting #AR #Isabelle
- Combining and automating classical and non-classical logics in classical higher-order logics #AR
- Rationality and escalation in infinite extensive games #Libro #RF #Coq
Lecturas de Junio de 2011
- Efficient interactive construction of machine-checked protocol security proofs in the context of dynamically compromising adversaries #TFM #RF #Isabelle
- Specification and verification: The Spec# experience #Verificación
- Formal verification of chess endgames tables #HOL4 #IA
- Integrating testing and interactive theorem proving #ACL2
- Conway’s games and some of their basic properties #Mizar
- A verified runtime for a verified theorem prover #HOL4
- Modelling distributed cognition systems in PVS #PVS
- Three chapters of measure theory in Isabelle/HOL #RF #Isabelle
- seL4 enforces integrity #Verificación #Isabelle
- Initial semantics for higher-order typed syntax in Coq #Coq
- Initial semantics for higher-order typed syntax in Coq #RF #Coq
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination #RF #Coq
- Specification of imperative languages using operational semantics in Coq #RF #Coq
- A first-order calculus for allegories #AR
- Generating schemata of resolution proofs #AR
- On the generation of positivstellensatz witnesses in degenerate cases #RF #Coq
- Deciding Kleene algebras in Coq #RF #Coq
- Glasgow Haskell vs. Lispworks #Haskell #Lisp
- On the expressive power of unit resolution #AR
- Proceedings 15th international refinement workshop #AR
- Solving the unsolvable #AR
- Type classes for efficient exact real arithmetic in Coq #Coq
- Un problema de las olimpiadas rusas en Haskell #Haskell
- BDDs verified in a proof assistant #Isabelle
- Embedding and automating conditional logics in classical higher-order logic.
- Incidence simplicial matrices formalized in Coq/SSReflect. #RF #Coq
- Isabelle repository for relational and algebraic methods #Isabelle
- Automated engineering of relational and algebraic methods in Isabelle/HOL #Isabelle
Lecturas de Julio de 2011
- SAT solver of Howe & King as a logic program #SAT #PL
- Razonamiento formalizado para la enseñanza de las matemáticas. #Enseñanza
- El problema de las puertas en Haskell. #Haskell
- Metadata for a mathematical wiki: Initial experiments. #Mizar
- Logical verification. #Coq
- Formal proofs for theoretical properties of Newton's method. #Coq
- Formalisation de la logique de description ALC dans l'assistant de preuve Coq. #Coq, #ALC
- Vérification d'une méthode de preuve pour la logique de description ALC. #Isabelle. #ALC
- A critique of Abelson and Sussman or why calculating is better than scheming. #Haskell, #Lisp
- Experiments with computable matrices in the Coq system. #Coq
- Computing the homology of groups: the geometric way. #Kenzo
- Peut-on faire des mathématiques avec un ordinateur?. #ME
- The theory behind TheoryMind. #Isabelle
- Provably correct conflict prevention bands algorithms. #PVS
- Peut-on avoir confiance en l'informatique?. #Verificación
- Automated theorem provers a practical tool for the working mathematician. #DAO
- Expresiones aritméticas mediante tipos abstracto de datos y polinomios. #Haskell
- A verified runtime for a verified theorem prover. #ACL2
- A framework for automated and certified refinement steps. #Isabelle
- Descomposiciones en sumas de cuadrados en Haskell. #Haskell
- Interactive proof introduction to IsabelleHOL. #Isabelle
- Coq au vin (The Coq proof assistant and the Curry-Howard correspondence) #Coq
- Hardware languages and proof. #Tesis #PVS #SAL
Lecturas de Agosto de 2011
- Theorem proving for verification (the early days) #Historia
- Selecting attributes for sport forecasting using formal concept analysis #AFC
- Formal methods: practice and experience #MF
- Automated deduction for verification #DAT
- Software model checking #Model_checking
- The verified software initiative: A Manifesto #Verificación
- How can i do that with ACL2 recent enhancements to ACL2 #ACL2
- Algebraic proofs over noncommutative formulas #Cálculo_polinomial
- Studies in algebraic and propositional proof complexity #Tesis #Cálculo_polinomial
- Formalization of an efficient representation of Bernstein polynomials and applications to global optimization #PVS
- Automating algebraic methods in Isabelle #Isabelle
- A repository for Tarski-Kleene Algebras #Isabelle
- Emergence and refinement #Emergencia, #Refinamentos
- Automated proving in geometry using Gröbner bases in Isabelle/HOL #Isabelle
- How efficient can fully verified functional programs be - A case study of graph traversal algorithms #Isabelle
- Imperative functional programming with Isabelle/HOL #Isabelle
- A flexible formal verification framework for industrial scale validation #ACL2
- Bit-blasting ACL2 theorems #ACL2 #GL
- A verified framework for symbolic execution in the ACL2 theorem prover. #ACL2 #GL
- Integrating testing and interactive theorem proving #ACL2
- seL4 enforces integrity #Isabelle
- Towards flight control verification using automated theorem proving #MetiTarski
- Ott: Effective tool support for the working semanticist. #Ott #Coq #Isabelle #HOL
- Lightweight tools for heavyweight semantics. #Lem #Ott #Coq #Isabelle #HOL
- Verifying SAT and SMT in Coq for a fully automated decision procedure. #Coq #SAT #SMT
- Maximum cardinality matching. #Isabelle
- Gauss-Jordan elimination for matrices represented as functions. #Isabelle
- Verification of dependable software using Spark and Isabelle. #Isabelle
- Verification of programs in virtual memory using separation logic. #Isabelle
- Automated specification analysis using an interactive theorem prover. #ACL2
- Formal analysis of fractional order systems in HOL. #HOL
Lecturas de Septiembre de 2011
- Formalization of abstract state transition systems for SAT. #Isabelle
- Zeno: A tool for the automatic verification of algebraic properties of functional programs #Isabelle #Haskell
- Automating induction with an SMT Solver. #SMT #Z3
- Artificial intelligence techniques for understanding gothic cathedrals #Prolog
- RDFS/OWL reasoning using the MapReduce framework. #DL #SW
- Automatic proof and disproof in Isabelle/HOL. #Isabelle
- Proof Pearl: Mechanizing the textbook proof of Huffman’s algorithm. #Isabelle
- Isabelle primer for mathematicians. #Isabelle
- Majority vote algorithm revisited again #Isabelle
- A survey on interactive theorem proving #Survey #ITP
- Formalization of Wu’s simple method in Coq. #Coq
- Functional programming for Java developers. #PF #Tutorial
- Formal verification for numerical methods. #Tesis #Coq
- Practical Semantic Web and linked data applications. Lisp edition. #SW #Lisp
- Basics of Coq. #Coq #Tutorial
- Coq in a hurry. #Coq #Tutorial
- Programación funcional con Haskell. #Haskell
- Ejercicios de programación funcional con Haskell. #Haskell
- Introducción a la programación lógica con Prolog. #Prolog
- Ejercicios de programación declarativa con Prolog. #Prolog
- Verification of the OWL-time ontology. #Prover9 #Ontología
- Proof Pearl: A formal proof of Higman’s lemma in ACL2. #ACL2
- Apprendre Haskell vous fera le plus grand bien!. #Haskell
- Implementation of Bourbaki's elements of mathematics in Coq: Part one, Theory of sets. #Coq
- Defining and using deductive systems with Isabelle. #Isabelle
- Some applications of propositional logic to cellular automata.
- Implementation of Bourbaki's elements of mathematics in Coq: Part Two; Ordered sets, Cardinals, integers. #Coq
- How Kenzo program works. #Kenzo
Lecturas de Octubre de 2011
- Automated reasoning: some successes and new challenges. #RA
- Generalized and formalized uncurrying. #Isabelle
- Basic first-order model theory in Mizar. #Mizar
- A certified module to study digital images with the Kenzo system. #ACL2
- What is a proof? #LI
- Proof Pearl: The marriage theorem. #Isabelle
- "Algorithms" is not a four-letter word. #Algorítmica
- An overview of methods for large-theory automated theorem proving #DAT.
- Haskell tutorial for C programmers. #Tutorial #Haskell
- Formalisation des courbes elliptiques en Coq. #Tesis #Coq
- Progress report on the ARC Project: Creating logical models of Gothic cathedrals. #IA #Prolog #RC
- OCaml for the masses: Why the next language you learn should be functional. #FP
Lecturas de Noviembre de 2011
- Efficient mergesort. #Isabelle #AFP
- Formalization of propositional linear temporal logic in the Mizar system. #Mizar
- Verification of certifying computations #Isabelle
- Coq, a proof assistant based on higher-order intuitionistic type theory. #Coq
- Retos y oportunidades de la IA en I+D+i con empresas. #IA
- Compositional verification of a communication protocol for a remotely operated vehicle. #PVS
- A definitional encoding of TLA* in Isabelle/HOL. #Isabelle
- VerSAT: a verified modern SAT solver. #GURU
- Towards automated system synthesis using SCIDUCTION. #Tesis
Lecturas de Diciembre de 2011
- Decision procedures for program synthesis and verification. #Tesis
- Grid based propositional satisfiability solving. #Tesis #SAT
- Partial mutual exclusion for infinitely many processes. #PVS
- Certifying algorithms. #Algoritmos_fehacientes
- A Proof Pearl with the fan theorem and bar induction (Walking through infinite trees with mixed induction and coinduction) #Coq
- Complex systems: A survey #Sistemas_complejos
- What is mathematical logic? A survey. #LI
- Knowledge representation and reasoning (Logic meets probability theory) #Libro #RC
- Construction des nombres algébriques réels en Coq. #Coq
- A methodology for the development and verification of expressive ontologies. #Tesis #Prover9
- Wave equation numerical resolution: mathematics and program. #Coq
- Étude de la différentiabilité et de l'intégrabilité en Coq (Application à la formule de d'Alembert pour l'équation des ondes) #Coq
- Formalizing a proof that e is transcendental. #HOL_Light
- A proof-theoretic account of primitive recursion and primitive iteration. #MinLog
- Initial semantics for higher-order typed syntax in Coq. #Coq
- Interactive theorem proving (A survey/tutorial, for logician). #Tutorial #ITP
- Can the computer really help us to prove theorems?. #ITP #Panorama
- An empirical study of errors in translating natural language into logic. #MDE
- The hardest logic puzzle ever. #Rompecabeza #LI