Diferencia entre revisiones de «Lecturas del año 2012»
Línea 1: | Línea 1: | ||
== Lecturas de Enero de 2012 == | == Lecturas de Enero de 2012 == | ||
− | * [http://interstices.info/jcms/int_63549/l-ordinateur-au-coeur-de-la-decouverte-mathematique L'ordinateur au cœur de la découverte mathématique]. | + | * [http://interstices.info/jcms/int_63549/l-ordinateur-au-coeur-de-la-decouverte-mathematique L'ordinateur au cœur de la découverte mathématique]. #Matematica_experimental |
− | * [http://bit.ly/uulX9N Últimos dos dígitos de (1+5^(2 | + | * [http://bit.ly/uulX9N Últimos dos dígitos de (1+5^(2*n+1))/6]. #Haskell |
− | |||
− | |||
* [http://arxiv.org/abs/1112.3782 Computing with hereditarily finite sequences]. #Prolog #MKM | * [http://arxiv.org/abs/1112.3782 Computing with hereditarily finite sequences]. #Prolog #MKM | ||
− | |||
− | |||
* [http://afp.sourceforge.net/entries/Markov_Models.shtml Markov models]. #Isabelle | * [http://afp.sourceforge.net/entries/Markov_Models.shtml Markov models]. #Isabelle | ||
* [http://bit.ly/xQa7rZ Turing machines] #Clásico #Divulgación | * [http://bit.ly/xQa7rZ Turing machines] #Clásico #Divulgación | ||
− | |||
* [http://www4.in.tum.de/~nipkow/pubs/vmcai12.pdf Teaching semantics with a proof assistant: No more LSD trip proofs]. #Isabelle #Enseñanza | * [http://www4.in.tum.de/~nipkow/pubs/vmcai12.pdf Teaching semantics with a proof assistant: No more LSD trip proofs]. #Isabelle #Enseñanza | ||
* [http://www.fing.edu.uy/~sierra/pres/2011/ciesc2008.pdf Enseñando deducción natural con Coq]. #Enseñanza #Lógica #Coq | * [http://www.fing.edu.uy/~sierra/pres/2011/ciesc2008.pdf Enseñando deducción natural con Coq]. #Enseñanza #Lógica #Coq | ||
Línea 20: | Línea 15: | ||
== Lecturas de Febrero de 2012 == | == Lecturas de Febrero de 2012 == | ||
− | |||
* [https://iist.unu.edu/sites/iist.unu.edu/files/biblio/report429.pdf Emergence and refinement]. #Sistemas_complejos | * [https://iist.unu.edu/sites/iist.unu.edu/files/biblio/report429.pdf Emergence and refinement]. #Sistemas_complejos | ||
* [http://www.springerlink.com/content/y222346j35g72064/fulltext.pdf Formalizing a hierarchical file system]. #PVS | * [http://www.springerlink.com/content/y222346j35g72064/fulltext.pdf Formalizing a hierarchical file system]. #PVS | ||
Línea 27: | Línea 21: | ||
* [http://www.nicta.com.au/pub?doc=5614 Formal system verification for trustworthy embedded systems]. #Isabelle | * [http://www.nicta.com.au/pub?doc=5614 Formal system verification for trustworthy embedded systems]. #Isabelle | ||
* [http://www.sciencedirect.com/science/article/pii/S1571066111000594 The mechanical verification of a DPLL-based satisfiability solver]. #PVS | * [http://www.sciencedirect.com/science/article/pii/S1571066111000594 The mechanical verification of a DPLL-based satisfiability solver]. #PVS | ||
− | |||
− | |||
− | |||
− | |||
− | |||
* [http://afp.sourceforge.net/entries/Refine_Monadic.shtml Refinement for monadic programs]. #Isabelle | * [http://afp.sourceforge.net/entries/Refine_Monadic.shtml Refinement for monadic programs]. #Isabelle | ||
* [http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml Dijkstra's shortest path algorithm]. #Isabelle | * [http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml Dijkstra's shortest path algorithm]. #Isabelle | ||
− | * [http://bit.ly/wV38h6 Computational topology]. | + | * [http://bit.ly/wV38h6 Computational topology]. #MC |
* [http://www.cs.st-andrews.ac.uk/~mik/categories.pdf Category theory and functional programming]. #Haskell | * [http://www.cs.st-andrews.ac.uk/~mik/categories.pdf Category theory and functional programming]. #Haskell | ||
− | |||
− | |||
* [http://www.math.pitt.edu/~thales/papers/turing.pdf Mathematics in the age of the Turing machine]. #Panorama #DAO | * [http://www.math.pitt.edu/~thales/papers/turing.pdf Mathematics in the age of the Turing machine]. #Panorama #DAO | ||
* [http://www.cl.cam.ac.uk/~mom22/itp12.pdf The reflective Milawa theorem prover is sound]. #ACL2 #HOL4 | * [http://www.cl.cam.ac.uk/~mom22/itp12.pdf The reflective Milawa theorem prover is sound]. #ACL2 #HOL4 | ||
Línea 57: | Línea 44: | ||
* [http://www.lri.fr/~paulin/LASER/course-notes.pdf Introduction to the Coq proof-assistant for practical software verification]. #Tutorial #Coq | * [http://www.lri.fr/~paulin/LASER/course-notes.pdf Introduction to the Coq proof-assistant for practical software verification]. #Tutorial #Coq | ||
* [http://www.lmcs-online.org/ojs/viewarticle.php?id=926&layout=abstract&iid=35 Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination] #Coq | * [http://www.lmcs-online.org/ojs/viewarticle.php?id=926&layout=abstract&iid=35 Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination] #Coq | ||
− | * [http://courses.csail.mit.edu/6.042/spring12/mcsfull.pdf Mathematics for | + | * [http://courses.csail.mit.edu/6.042/spring12/mcsfull.pdf Mathematics for computer science]. #Libro |
* [http://www21.in.tum.de/~popescua/pos.pdf Proving possibilistic, probabilistic noninterference]. #Isabelle | * [http://www21.in.tum.de/~popescua/pos.pdf Proving possibilistic, probabilistic noninterference]. #Isabelle | ||
− | * [http://bit.ly/xH1KJy Decision procedures in | + | * [http://bit.ly/xH1KJy Decision procedures in algebra and logic (Reading material)]. #Libro #Lógica |
* [http://cgi.cse.unsw.edu.au/~rvg/eptcs/Published/LSFA2011/Papers/7/paper/AvelarAyalaRincon-1.pdf A formalization of the theorem of existence of first-order most general unifiers]. #PVS | * [http://cgi.cse.unsw.edu.au/~rvg/eptcs/Published/LSFA2011/Papers/7/paper/AvelarAyalaRincon-1.pdf A formalization of the theorem of existence of first-order most general unifiers]. #PVS | ||
Línea 68: | Línea 55: | ||
* [http://www.springerlink.com/content/4t355540232364p2/ PVS linear algebra libraries for verification of control software algorithms in C/ACSL]. #PVS | * [http://www.springerlink.com/content/4t355540232364p2/ PVS linear algebra libraries for verification of control software algorithms in C/ACSL]. #PVS | ||
* [http://www.springerlink.com/content/g520875717744612/ Generating verifiable Java code from verified PVS specifications]. #PVS | * [http://www.springerlink.com/content/g520875717744612/ Generating verifiable Java code from verified PVS specifications]. #PVS | ||
− | * [http://www.cs.nott.ac.uk/~bmv/Papers/tfp2012_abstract.pdf Haskell gets argumentative]. #Haskell #Lógica | + | * [http://www.cs.nott.ac.uk/~bmv/Papers/tfp2012_abstract.pdf Haskell gets argumentative]. #Haskell #Lógica #IA |
− | * [http://education.lms.ac.uk/wp-content/uploads/2012/02/David_Pierce.pdf Induction and recursion]. #Fundamentos | + | * [http://education.lms.ac.uk/wp-content/uploads/2012/02/David_Pierce.pdf Induction and recursion]. #Fundamentos #LI |
* [http://www.cse.chalmers.se/~siles/papers/sasaki-murao.pdf A formal proof of Sasaki-Murao algorithm]. #Coq | * [http://www.cse.chalmers.se/~siles/papers/sasaki-murao.pdf A formal proof of Sasaki-Murao algorithm]. #Coq | ||
* [http://r6.ca/Goedel/goedel1.html Essential incompleteness of arithmetic verified by Coq]. #Coq | * [http://r6.ca/Goedel/goedel1.html Essential incompleteness of arithmetic verified by Coq]. #Coq | ||
* [http://r6.ca/Thesis/ Incompleteness & completeness: Formalizing logic and analysis in type theory]. #Tesis #Coq | * [http://r6.ca/Thesis/ Incompleteness & completeness: Formalizing logic and analysis in type theory]. #Tesis #Coq | ||
* [http://afp.sourceforge.net/devel-entries/Well_Quasi_Orders.shtml Well-quasi-orders]. #Isabelle | * [http://afp.sourceforge.net/devel-entries/Well_Quasi_Orders.shtml Well-quasi-orders]. #Isabelle | ||
− | * [http://www.irisa.fr/celtique/genet/ACF/ Analyse et | + | * [http://www.irisa.fr/celtique/genet/ACF/ Analyse et conception formelles (Software formal analysis and design)]. #Curso #Isabelle |
== Lecturas de Mayo de 2012 == | == Lecturas de Mayo de 2012 == | ||
Línea 84: | Línea 71: | ||
* [http://kuscholarworks.ku.edu/dspace/handle/1808/8037 HaskHOL: A Haskell hosted domain specific language for Higher-Order Logic theorem proving]. #Tesis #Haskell | * [http://kuscholarworks.ku.edu/dspace/handle/1808/8037 HaskHOL: A Haskell hosted domain specific language for Higher-Order Logic theorem proving]. #Tesis #Haskell | ||
* [http://cdn.bitbucket.org/jhlchan/hol/downloads/fermatProof.pdf A string of pearls: proofs of Fermat's little theorem]. #HOL4 | * [http://cdn.bitbucket.org/jhlchan/hol/downloads/fermatProof.pdf A string of pearls: proofs of Fermat's little theorem]. #HOL4 | ||
− | |||
− | |||
* [http://afp.sourceforge.net/entries/Separation_Algebra.shtml Separation algebra]. #Isabelle | * [http://afp.sourceforge.net/entries/Separation_Algebra.shtml Separation algebra]. #Isabelle | ||
* [http://www.eecs.qmul.ac.uk/~masci/works/preprints/preprint-ISSE-modelling_DC_in_PVS-embedded_refs-V1.pdf Using PVS to support the analysis of distributed cognition systems]. #PVS | * [http://www.eecs.qmul.ac.uk/~masci/works/preprints/preprint-ISSE-modelling_DC_in_PVS-embedded_refs-V1.pdf Using PVS to support the analysis of distributed cognition systems]. #PVS | ||
Línea 91: | Línea 76: | ||
* [http://www.ece.concordia.ca/~o_hasan/thesis_hasan.pdf Formal probabilistic analysis using theorem proving]. #Tesis #HOL | * [http://www.ece.concordia.ca/~o_hasan/thesis_hasan.pdf Formal probabilistic analysis using theorem proving]. #Tesis #HOL | ||
* [http://web.student.chalmers.se/~danr/master-thesis-draft.pdf Proving equational Haskell properties using automated theorem provers]. #Haskell #Thesis | * [http://web.student.chalmers.se/~danr/master-thesis-draft.pdf Proving equational Haskell properties using automated theorem provers]. #Haskell #Thesis | ||
− | * [http://cps-vo.org/node/3338 Accessible integrated formal reasoning environments in classroom instruction of mathematics]. | + | * [http://cps-vo.org/node/3338 Accessible integrated formal reasoning environments in classroom instruction of mathematics]. #Enseñanza |
− | * [http://cs-people.bu.edu/lapets/resource/dalfvs.pdf Designing accessible lightweight formal verification systems | + | * [http://cs-people.bu.edu/lapets/resource/dalfvs.pdf Designing accessible lightweight formal verification systems]. #AR |
− | |||
* [http://web.student.chalmers.se/~danr/hipspec-atx.pdf HipSpec: Automating inductive proofs of program properties]. #Haskell | * [http://web.student.chalmers.se/~danr/hipspec-atx.pdf HipSpec: Automating inductive proofs of program properties]. #Haskell | ||
* [http://www.cs.toronto.edu/~hector/tc-instructor.html Supplementary material for "Thinking as computation"]. #IA #Prolog | * [http://www.cs.toronto.edu/~hector/tc-instructor.html Supplementary material for "Thinking as computation"]. #IA #Prolog | ||
Línea 99: | Línea 83: | ||
* [http://www.ssrg.nicta.com.au/publications/papers/Greenaway_AK_12.pdf Bridging the gap: Automatic verified abstraction of C] | * [http://www.ssrg.nicta.com.au/publications/papers/Greenaway_AK_12.pdf Bridging the gap: Automatic verified abstraction of C] | ||
* [http://faculty.cs.byu.edu/~jay/static/toronto-2012flops.pdf Computing in Cantor’s paradise with λZFC]. | * [http://faculty.cs.byu.edu/~jay/static/toronto-2012flops.pdf Computing in Cantor’s paradise with λZFC]. | ||
− | |||
* [http://www.lri.fr/~mcg/PDF/VSSTE2012.pdf Isabelle/Circus: A process specification and verification environment]. #Isabelle | * [http://www.lri.fr/~mcg/PDF/VSSTE2012.pdf Isabelle/Circus: A process specification and verification environment]. #Isabelle | ||
* [http://afp.sourceforge.net/entries/Circus.shtml Isabelle/Circus]. #Isabelle | * [http://afp.sourceforge.net/entries/Circus.shtml Isabelle/Circus]. #Isabelle | ||
Línea 148: | Línea 131: | ||
* [http://www.cs.princeton.edu/~rdockins/dissertation/thesis-online.pdf Operational refinement for compiler correctness]. #Tesis #Coq | * [http://www.cs.princeton.edu/~rdockins/dissertation/thesis-online.pdf Operational refinement for compiler correctness]. #Tesis #Coq | ||
* [http://www.irit.fr/~Martin.Strecker/Publications/proofs_graph_transformations.html Interactive and automated proofs for graph transformations]. #Isabelle | * [http://www.irit.fr/~Martin.Strecker/Publications/proofs_graph_transformations.html Interactive and automated proofs for graph transformations]. #Isabelle | ||
− | |||
* [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. #Haskell | * [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. #Haskell | ||
* [http://blogs.elpais.com/turing/2012/09/computadores-von-neumann-o-computadores-turing.html ¿Computadores von Neumann, o computadores Turing?] #Historia | * [http://blogs.elpais.com/turing/2012/09/computadores-von-neumann-o-computadores-turing.html ¿Computadores von Neumann, o computadores Turing?] #Historia | ||
Línea 157: | Línea 139: | ||
* [http://hal.inria.fr/hal-00712938/PDF/article.pdf Improving real analysis in Coq: a user-friendly approach to integrals and derivatives]. #Coq ([http://cpp12.kuis.kyoto-u.ac.jp/accepted.html CPP2012]) | * [http://hal.inria.fr/hal-00712938/PDF/article.pdf Improving real analysis in Coq: a user-friendly approach to integrals and derivatives]. #Coq ([http://cpp12.kuis.kyoto-u.ac.jp/accepted.html CPP2012]) | ||
* [http://www.cse.chalmers.se/~mortberg/papers/cphwcs.pdf Computing persistent homology within Coq/SSReflect]. #Coq | * [http://www.cse.chalmers.se/~mortberg/papers/cphwcs.pdf Computing persistent homology within Coq/SSReflect]. #Coq | ||
− | |||
* [http://www.cse.chalmers.se/~siles/papers/sasaki-murao.pdf A formal proof of Sasaki-Murao algorithm]. #Coq ([http://www.map2012.uni-konstanz.de/ MAP2012], [http://www.cse.chalmers.se/~siles/coq/formalisation.html code], [http://www.cse.chalmers.se/~mortberg/talks/anders-map2012.pdf Presentación]). | * [http://www.cse.chalmers.se/~siles/papers/sasaki-murao.pdf A formal proof of Sasaki-Murao algorithm]. #Coq ([http://www.map2012.uni-konstanz.de/ MAP2012], [http://www.cse.chalmers.se/~siles/coq/formalisation.html code], [http://www.cse.chalmers.se/~mortberg/talks/anders-map2012.pdf Presentación]). | ||
Línea 169: | Línea 150: | ||
* [http://hal.inria.fr/docs/00/74/30/90/PDF/article.pdf A formally-verified C compiler supporting floating-point arithmetic]. #Coq | * [http://hal.inria.fr/docs/00/74/30/90/PDF/article.pdf A formally-verified C compiler supporting floating-point arithmetic]. #Coq | ||
* [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/BoyerMoore.pdf The Boyer-Moore waterfall model revisited]. #HOL_Light | * [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/BoyerMoore.pdf The Boyer-Moore waterfall model revisited]. #HOL_Light | ||
− | |||
== Lecturas de Noviembre de 2012 == | == Lecturas de Noviembre de 2012 == | ||
Línea 197: | Línea 177: | ||
== Lecturas de Diciembre de 2012 == | == Lecturas de Diciembre de 2012 == | ||
− | |||
* [http://arxiv.org/pdf/1211.6197 Verifying probabilistic correctness in Isabelle with pGCL]. #Isabelle | * [http://arxiv.org/pdf/1211.6197 Verifying probabilistic correctness in Isabelle with pGCL]. #Isabelle | ||
* [http://www.ceciis.foi.hr/app/public/conferences/1/papers2012/dkb3.pdf Formalization of a strategy for the KRK chess endgame]. #Coq | * [http://www.ceciis.foi.hr/app/public/conferences/1/papers2012/dkb3.pdf Formalization of a strategy for the KRK chess endgame]. #Coq | ||
Línea 206: | Línea 185: | ||
* [http://www.irit.fr/~Ralph.Matthes/papers/MatthesPicardTYPES11PostProc.pdf Verification of redecoration for infinite triangular matrices using coinduction]. #Coq | * [http://www.irit.fr/~Ralph.Matthes/papers/MatthesPicardTYPES11PostProc.pdf Verification of redecoration for infinite triangular matrices using coinduction]. #Coq | ||
* [http://www.irit.fr/~Celia.Picard/These/ Représentation coinductive des graphes]. #Tesis #Coq | * [http://www.irit.fr/~Celia.Picard/These/ Représentation coinductive des graphes]. #Tesis #Coq | ||
− | * [http://link.springer.com/content/pdf/10.1007%2Fs10817-012-9268-z Formal mathematics for mathematicians]. | + | * [http://link.springer.com/content/pdf/10.1007%2Fs10817-012-9268-z Formal mathematics for mathematicians]. #RA |
* [http://link.springer.com/article/10.1007/s10817-012-9250-9 The HOL Light theory of euclidean space]. #HOL_Light | * [http://link.springer.com/article/10.1007/s10817-012-9250-9 The HOL Light theory of euclidean space]. #HOL_Light | ||
* [http://link.springer.com/content/pdf/10.1007%2Fs10817-012-9265-2 Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar]. #Mizar | * [http://link.springer.com/content/pdf/10.1007%2Fs10817-012-9265-2 Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar]. #Mizar | ||
Línea 213: | Línea 192: | ||
* [http://arxiv.org/pdf/1212.3870v1 Interactive verification of Markov chains: Two distributed protocol case studies]. #Isabelle | * [http://arxiv.org/pdf/1212.3870v1 Interactive verification of Markov chains: Two distributed protocol case studies]. #Isabelle | ||
* [http://interstices.info/jcms/int_63417/du-reve-a-la-realite-des-preuves Du rêve à la réalité des preuves]. (Interstices, 2012) #Divulgación #DAO | * [http://interstices.info/jcms/int_63417/du-reve-a-la-realite-des-preuves Du rêve à la réalité des preuves]. (Interstices, 2012) #Divulgación #DAO | ||
− | * [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation] | + | * [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation] #RA |
Revisión actual del 06:32 28 abr 2013
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. #Matematica_experimental
- Últimos dos dígitos de (1+5^(2*n+1))/6. #Haskell
- Computing with hereditarily finite sequences. #Prolog #MKM
- Markov models. #Isabelle
- Turing machines #Clásico #Divulgación
- 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
- 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
- Refinement for monadic programs. #Isabelle
- Dijkstra's shortest path algorithm. #Isabelle
- Computational topology. #MC
- Category theory and functional programming. #Haskell
- 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 #LI
- 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 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. #Enseñanza
- Designing accessible lightweight formal verification systems. #AR
- 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.
- 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
- 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
- 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
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
- 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. #RA
- 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 #RA