Diferencia entre revisiones de «Lecturas del año 2011»
(→Lecturas de Enero de 2011) |
|||
| Línea 26: | Línea 26: | ||
* [http://bit.ly/gZYKNJ Lectures in game theory for computer scientists] #Libro | * [http://bit.ly/gZYKNJ Lectures in game theory for computer scientists] #Libro | ||
* [http://bit.ly/dNvlXU Reactive valuations] #TFM | * [http://bit.ly/dNvlXU Reactive valuations] #TFM | ||
| − | * [http://slidesha.re/f8SKgI Oportunidades para la economía basada en la Ingeniería del Conocimiento en Internet] | + | * [http://slidesha.re/f8SKgI Oportunidades para la economía basada en la Ingeniería del Conocimiento en Internet] |
| + | * [http://bit.ly/haeTax Algunas aplicaciones de las bases de Groebner] | ||
* [http://bit.ly/hrwBXD Programación funcional con Haskell] #Libro #Haskell | * [http://bit.ly/hrwBXD Programación funcional con Haskell] #Libro #Haskell | ||
* [http://bit.ly/eGqBDZ Certifying compilers using higher-order theorem provers as certificate checker] #Isabelle #Coq | * [http://bit.ly/eGqBDZ Certifying compilers using higher-order theorem provers as certificate checker] #Isabelle #Coq | ||
| Línea 34: | Línea 35: | ||
* [http://bit.ly/eZiRVL Deducción natural en lógica proposicional con Isabelle/Isar] #Isabelle #V | * [http://bit.ly/eZiRVL Deducción natural en lógica proposicional con Isabelle/Isar] #Isabelle #V | ||
* [http://bit.ly/hTYRXf Deducción natural en lógica de primer orden con Isabelle/Isar] #Isabelle #V | * [http://bit.ly/hTYRXf Deducción natural en lógica de primer orden con Isabelle/Isar] #Isabelle #V | ||
| − | * [http://bit.ly/h2co0D | + | * [http://bit.ly/h2co0D fKenzo: A user interface for computations in Algebraic Topology] |
| − | |||
| − | |||
* [http://bit.ly/hZdkPN A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL]. #Isabelle | * [http://bit.ly/hZdkPN A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL]. #Isabelle | ||
* [http://bit.ly/gcvJNz El tipo abstracto de datos de las colas de prioridad en Haskell] #Haskell #V | * [http://bit.ly/gcvJNz El tipo abstracto de datos de las colas de prioridad en Haskell] #Haskell #V | ||
| Línea 61: | Línea 60: | ||
* [http://bit.ly/hBKzIz El tipo abstracto de datos de las colas en Haskell] #Haskell #V | * [http://bit.ly/hBKzIz El tipo abstracto de datos de las colas en Haskell] #Haskell #V | ||
* [http://goo.gl/oUlcY Executable transitive closures of finite relations] #RF #Isabelle | * [http://goo.gl/oUlcY Executable transitive closures of finite relations] #RF #Isabelle | ||
| − | * [http://goo.gl/epNrc | + | * [http://goo.gl/epNrc Solución española para un problema de John Nash] |
| − | + | + [http://goo.gl/FoL94 Reduced ordered binary decision diagram with implied literals: A new knowledge compilation approach] #AR | |
| − | |||
* [http://bit.ly/gHpfXL Teaching FP to freshmen] #Enseñanza #PF | * [http://bit.ly/gHpfXL Teaching FP to freshmen] #Enseñanza #PF | ||
* [http://goo.gl/2fK3d Introduction to artificial intelligence] #Libro #IA | * [http://goo.gl/2fK3d Introduction to artificial intelligence] #Libro #IA | ||
| Línea 191: | Línea 189: | ||
* [http://bit.ly/oe6zF6 Peut-on avoir confiance en l'informatique?]. #Verificación | * [http://bit.ly/oe6zF6 Peut-on avoir confiance en l'informatique?]. #Verificación | ||
* [http://bit.ly/pzjDet Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011)]. #GLC, #Vestigium | * [http://bit.ly/pzjDet Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011)]. #GLC, #Vestigium | ||
| − | * [~/BibliotecaDigital/Bundy_2011_Automated theorem provers a practical tool for the working mathematician.pdf Automated theorem provers a practical tool for the working mathematician]. #DAO, #Vestigium | + | * [http://www.glc.cs.us.es/~jalonso/BibliotecaDigital/Bundy_2011_Automated theorem provers a practical tool for the working mathematician.pdf Automated theorem provers a practical tool for the working mathematician]. #DAO, #Vestigium |
* [http://www.phdcomics.com/comics.php?f=1436 Intellectual Freedom]. #Humor | * [http://www.phdcomics.com/comics.php?f=1436 Intellectual Freedom]. #Humor | ||
* [http://bit.ly/q4rgao Expresiones aritméticas mediante tipos abstracto de datos y polinomios]. #Haskell, #Vestigium | * [http://bit.ly/q4rgao Expresiones aritméticas mediante tipos abstracto de datos y polinomios]. #Haskell, #Vestigium | ||
| Línea 233: | Línea 231: | ||
* [http://arxiv.org/pdf/1108.3446v1 Premise selection for mathematics by corpus analysis and kernel methods]. #AA | * [http://arxiv.org/pdf/1108.3446v1 Premise selection for mathematics by corpus analysis and kernel methods]. #AA | ||
* [http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml Gauss-Jordan elimination for matrices represented as functions]. #Isabelle | * [http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml Gauss-Jordan elimination for matrices represented as functions]. #Isabelle | ||
| − | * [Verification of dependable software using Spark and Isabelle]. #Isabelle | + | * [http://goo.gl/LyRYt Verification of dependable software using Spark and Isabelle]. #Isabelle |
| − | * [Verification of programs in virtual memory using separation logic]. #Isabelle | + | * [http://goo.gl/W6eUw Verification of programs in virtual memory using separation logic]. #Isabelle |
| − | * [Automated specification analysis using an interactive theorem prover]. #ACL2 | + | * [http://goo.gl/zWkeU Automated specification analysis using an interactive theorem prover]. #ACL2 |
| − | * [Formal analysis of fractional order systems in HOL]. #HOL | + | * [http://goo.gl/C6HfW Formal analysis of fractional order systems in HOL]. #HOL |
== Lecturas de Septiembre de 2011 == | == Lecturas de Septiembre de 2011 == | ||
| − | * [Formalization of abstract state transition systems for SAT]. #Isabelle | + | * [http://goo.gl/fRfbP Formalization of abstract state transition systems for SAT]. #Isabelle |
* [http://bit.ly/pmJLlD Zeno: A tool for the automatic verification of algebraic properties of functional programs] #Isabelle #Haskell | * [http://bit.ly/pmJLlD Zeno: A tool for the automatic verification of algebraic properties of functional programs] #Isabelle #Haskell | ||
* [http://research.microsoft.com/en-us/um/people/leino/papers/krml218.pdf Automating induction with an SMT Solver]. #SMT #Z3 | * [http://research.microsoft.com/en-us/um/people/leino/papers/krml218.pdf Automating induction with an SMT Solver]. #SMT #Z3 | ||
| Línea 313: | Línea 311: | ||
* [http://jfr.cib.unibo.it/article/view/2225 A proof-theoretic account of primitive recursion and primitive iteration]. #MinLog | * [http://jfr.cib.unibo.it/article/view/2225 A proof-theoretic account of primitive recursion and primitive iteration]. #MinLog | ||
* [http://jfr.cib.unibo.it/article/view/2066 Initial semantics for higher-order typed syntax in Coq]. #Coq | * [http://jfr.cib.unibo.it/article/view/2066 Initial semantics for higher-order typed syntax in Coq]. #Coq | ||
| − | * [ | + | * [http://www.ams.org/notices/200807/tx080700773p.pdf Desperately seeking mathematical truth]. #Filosofia |
* [http://www.andrew.cmu.edu/user/avigad/Talks/ioannina.pdf Interactive theorem proving (A survey/tutorial, for logician)]. #Tutorial #ITP | * [http://www.andrew.cmu.edu/user/avigad/Talks/ioannina.pdf Interactive theorem proving (A survey/tutorial, for logician)]. #Tutorial #ITP | ||
* [http://www.cs.ru.nl/~herman/ictopen.pdf Can the computer really help us to prove theorems?]. #ITP #Panorama | * [http://www.cs.ru.nl/~herman/ictopen.pdf Can the computer really help us to prove theorems?]. #ITP #Panorama | ||
* [http://ggweb.stanford.edu/assets/ctx/1.0-SNAPSHOT/downloads/TechReports/OP-Cogsci-2008.pdf An empirical study of errors in translating natural language into logic]. #MDE | * [http://ggweb.stanford.edu/assets/ctx/1.0-SNAPSHOT/downloads/TechReports/OP-Cogsci-2008.pdf An empirical study of errors in translating natural language into logic]. #MDE | ||
* [http://www.hcs.harvard.edu/~hrp/issues/1996/Boolos.pdf The hardest logic puzzle ever]. #Rompecabeza | * [http://www.hcs.harvard.edu/~hrp/issues/1996/Boolos.pdf The hardest logic puzzle ever]. #Rompecabeza | ||
Revisión del 19:39 27 abr 2013
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
- Does Godel's theorem matter to mathematics?
- Distributed SAT. #SAT
- Semantic web reasoners and languages #WS
- El 2011 y los números primos (en Haskell) #Haskell #V
- The dialectica interpertation in Coq #Coq
- Errores aritméticos en Haskell y en Lisp #Haskell #Lisp #V
- 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 #V
- 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.
- Algorithms take control of Wall Street #IA
- Formal reliability analysis of combinational circuits using theorem proving #HOL
- Determinación, esperanza y éxitos en la resolución de problemas #Enseñanza #V
- Lectures in game theory for computer scientists #Libro
- Reactive valuations #TFM
- Oportunidades para la economía basada en la Ingeniería del Conocimiento en Internet
- Algunas aplicaciones de las bases de Groebner
- 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 #V
Lecturas de Febrero de 2011
- Deducción natural en lógica proposicional con Isabelle/Isar #Isabelle #V
- Deducción natural en lógica de primer orden con Isabelle/Isar #Isabelle #V
- fKenzo: A user interface for computations in Algebraic Topology
- 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 #V
- Program verification and functioning of operative computing revisited: How about mathematics engineering? #Verificación
- El próximo después de 1811 #Haskell #V
- Humanos más capaces y robots que están en las nubes #IA
- 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) #V
- Inconsistent heuristics in theory and practice #IA
- On proof and progress in mathematics #CM
- Artificial intelligence (Foundations of computational agents) #Libro #IA
- Are mathematicians in Jeopardy? #IA
- Give me that good old-fashioned AI #IA
- Building Watson: An overview of the deepQA project #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 #V
- El tipo abstracto de datos de las pilas en Haskell #Haskell #V
- El tipo abstracto de datos de las colas en Haskell #Haskell #V
- Executable transitive closures of finite relations #RF #Isabelle
- Solución española para un problema de John Nash
+ Reduced ordered binary decision diagram with implied literals: A new knowledge compilation approach #AR
- Teaching FP to freshmen #Enseñanza #PF
- Introduction to artificial intelligence #Libro #IA
- La Universidad Carnegie-Mellon elimina la programación OO de su primer curso #Enseñanza
- Experience report: Functional programming through deep Time (Modeling the first complex ecosystems on Earth) #Haskell
- A comparative study on ILP-based concept discovery systems #ILP
- 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
- Artificial intelligence and human thinking #IA
- 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
- Los matemáticos no buscan resultados, van tras la belleza #CM
- 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
- How to read a mathematics textbook #Enseñanza
- 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
- Numbers as data structures: the prime successor function as primitive #Enseñanza
- 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
- On a strongly normalizing STG machine #Tesis
- 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 #V
- 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
- Entusiasmo, clave del buen maestro #Enseñanza
- 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
- 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
- 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 #V
- 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
- What’s fun about teaching #Enseñanza
- 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. #Vestigium, #Enseñanza
- The ideal mathematician. #Humor
- 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
- Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011). #GLC, #Vestigium
- theorem provers a practical tool for the working mathematician.pdf Automated theorem provers a practical tool for the working mathematician. #DAO, #Vestigium
- Intellectual Freedom. #Humor
- Expresiones aritméticas mediante tipos abstracto de datos y polinomios. #Haskell, #Vestigium
- 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, #Vestigium
- 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
- Lecturas del Grupo de Lógica Computacional (Julio de 2011). #GLC #Vestigium
- Formal methods: practice and experience #Métodos formales
- 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
- Markets are efficient if and only if P = NP.
- 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
- Peirce's truth-functional analysis and the origin of truth tables. #Historia
- 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
- Premise selection for mathematics by corpus analysis and kernel methods. #AA
- 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
- Reasoning processes in propositional logic.
- 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.
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?
- Los peligros de “pagar por publicar” en las revistas científicas de acceso abierto.
- The dangers of the “author pays” model in mathematical publishing.
- 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.
- Lecturas del Grupo de Lógica Computacional (Septiembre de 2011)
- 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
- What is mathematical logic? A survey.
- Knowledge representation and reasoning (Logic meets probability theory) #Libro
- 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
- Desperately seeking mathematical truth. #Filosofia
- 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
