{"id":4945,"date":"2015-07-16T07:24:05","date_gmt":"2015-07-16T05:24:05","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4945"},"modified":"2015-07-16T07:24:05","modified_gmt":"2015-07-16T05:24:05","slug":"lecturas-del-grupo-de-logica-computacional-desde-el-29-de-junio-de-2014","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lecturas-del-grupo-de-logica-computacional-desde-el-29-de-junio-de-2014\/","title":{"rendered":"Lecturas del Grupo de L\u00f3gica Computacional (desde el 29 de junio de 2014)"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas este curso (del 29 de junio de 2014 al 15 de julio de 2015) en<br \/>\n<a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a> sobre l\u00f3gica computacional y programaci\u00f3n funcional.<\/p>\n<p>Al final de cada art\u00edculo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.<\/p>\n<ul>\n<li><a href=\"http:\/\/bit.ly\/1ISzLUm\">A Coq formalization of a sign determination algorithm in real algebraic geometry<\/a>. ~ C. Cohen &amp; M. Kohli #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Q0Q1Bz\">A Haskell implementation of a rule-based program transformation for C programs<\/a>. ~ S. Tamarit et als. #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1zvJoox\">A Haskell monad for infinite search in finite time<\/a>. ~ M. Escardo #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1zITU8N\">A combinator library for MCMC sampling<\/a>. ~ P. Narayanan &amp; C.C. Shan #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1r1Fwmi\">A concrete deskolemization algorithm<\/a>. ~ R. van Sparrentak #Logic #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1yr1s1n\">A constructive semantics for rewriting logic<\/a>. ~ M.N. Kaplan #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1quqghx\">A course in Haskell-based software testing<\/a>. ~ J. van Eijck &amp; V. Zaytsev #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1zpAw33\">A formal and constructive theory of computation<\/a>. ~ Y. Forster #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1w9pWWG\">A formal proof of the Kepler conjecture<\/a>. ~ T. Hales et als. #ITP #HOL_LIght #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1D4RsYw\">A formal verification of the theory of parity complexes<\/a>. ~ M. Buckley #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1y3gSZM\">A formalisation of Sturm\u2019s theorem<\/a>. ~ M. Eberl #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1J8iYvr\">A formalisation of finite automata using hereditarily finite sets<\/a>. ~ L.C. Paulson #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1rrC3xo\">A formalization in Coq of Edwardk Kmett\u2019s Hask library for Haskell<\/a>. ~ J. Wiegley &amp; E. Kmett #ITP #Coq #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ed1qmD\">A formalization of strand spaces in Coq<\/a>. ~ Hai Nguyen #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ISAJAb\">A formalized hierarchy of probabilistic system types<\/a>. ~ J. H\u00f6lzl, A. Lochbihler &amp; D. Traytel #Isabelle_HOL #ITP <\/li>\n<li><a href=\"http:\/\/bit.ly\/14JbZbQ\">A formally-verified C static analyzer<\/a>. ~ J.H. Jourdan et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/1.usa.gov\/1quLW0Q\">A formally-verified decision procedure for univariate polynomial computation based on Sturm\u2019s Theorem<\/a>. ~ C. Mu\u00f1oz et al. #PVS<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GdWHck\">A framework for developing stand-alone certifiers<\/a>. ~ C. Sternagel &amp; R. Thiemann #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1J88mN5\">A framework for exploring finite models<\/a>. ~ S. Saghafi #PhD_Thesis #Logic #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Bg6hJ4\">A framework for verified depth-first algorithms<\/a>. ~ R. Neumann #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1i5Kn6a\">A generic numbering system based on Catalan families of combinatorial objects<\/a>. ~ P. Tarau #Haskell <\/li>\n<li><a href=\"http:\/\/bit.ly\/1J8b05w\">A mechanisation of internal Galois connections in order theory formalised without meets<\/a>. ~ M. Al-Hassy #Agda<\/li>\n<li><a href=\"http:\/\/bit.ly\/14pM6gr\">A mechanised proof of G\u00f6del&#8217;s incompleteness theorems using Nominal Isabelle<\/a>. ~ L.C. Paulson #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1lR2mKm\">A mechanized verification environment for real-time process algebras and low-level programming languages<\/a>. ~ B. Bartels #Thesis #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GtosAc\">A nominal exploration of intuitionism<\/a>. ~ V. Rahli &amp; M. Bickford #ITP #Nuprl<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Cj45Aq\">A pilot study of the use of LogEx, lessons learned<\/a>. ~ J. Lodder, B. Heeren &amp; J. Jeuring #Logic<\/li>\n<li><a href=\"http:\/\/bit.ly\/1IdKtmr\">A primer on Homotopy Type Theory (Part 1: The formal type theory)<\/a>. ~ J. Ladyman &amp; S. Presnell #HoTT<\/li>\n<li><a href=\"http:\/\/bit.ly\/VENgAm\">A semantics for intuitionistic higher-order logic supporting higher-order abstract syntax<\/a>. ~ C.E. Brown #Logic #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1NnZy4m\">A typechecker plugin for units of measure (Domain-specific constraint solving in GHC Haskell)<\/a>. ~ A. Gundry #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1su0mwF\">A typed C11 semantics for interactive theorem proving<\/a>. ~ R. Krebbers &amp; F. Wiedijk #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1IUtFR6\">A verified enclosure for the Lorenz attractor (Rough diamond)<\/a>. ~ F. Immler #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1y3hEGo\">Affine arithmetic<\/a>. ~ F. Immler #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1qqBHti\">Amortized complexity verified<\/a>. ~ T. Nipkow #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1DlYTQn\">An intrinsic encoding of a subset of C and its application to TLS network packet processing<\/a>. ~ R. Affeldt &amp; K. Sakaguchi #Coq <\/li>\n<li><a href=\"http:\/\/bit.ly\/1Gxxmx6\">An introduction to proof assistants<\/a>. ~ P. Schnider #ITP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1kp4XzJ\">An investigation into the use of Haskell for dynamic programming<\/a>. ~ D. McGillicuddy, A.J. Parkes &amp; H. Nilsson #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1D4ShjT\">An overabundance of equality: Implementing kind equalities into Haskell<\/a>. ~ R.A. Eisenberg #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1BRh01v\">Applicative bidirectional programming with lenses<\/a>. ~ K. Matsuda &amp; M. Wang #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1DOnDjX\">Au del\u00e0 des r\u00e9els: m\u00e9thodes num\u00e9riques en informatique<\/a>. ~ G. Connan #eBook #Math #Haskell <\/li>\n<li><a href=\"http:\/\/bit.ly\/1AGFXHB\">Automated generation of machine verifiable and readable proofs: A case study of Tarski\u2019s geometry<\/a>. ~ J. Narboux et als. #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/18d3wyK\">Automated verification of role-based access control policies constraints using Prover9<\/a>. ~ K.E. Sabri #ATP #Prover9<\/li>\n<li><a href=\"http:\/\/bit.ly\/1LxLbLz\">Automatic and transparent transfer of theorems along isomorphisms in the Coq proof assistant<\/a>. ~ T. Zimmermann &amp; H. Herbelin #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1nsC8nG\">Automatically verified implementation of data structures based on AVL trees<\/a>. ~ M. Clochard #Why3<\/li>\n<li><a href=\"http:\/\/bit.ly\/1EvPpi6\">Automating change of representation for proofs in discrete mathematics<\/a>. ~ D. Raggi, A. Bundy, G. Grov &amp; A. Pease #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/13mJLCt\">Automating formal proofs for reactive systems<\/a>. ~ D. Ricketts et als. #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1sZK2k2\">Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light<\/a>. ~ L. Michel #HOL_Light<\/li>\n<li><a href=\"http:\/\/bit.ly\/15e7yXi\">Bind induction: Extracting monadic programs from proofs<\/a>. ~ H. Shafei &amp; J. Caldwell #Haskell #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Cj26Ok\">Bounded refinement types<\/a>. ~ N. Vazou, A. Bakst &amp; R. Jhala #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Qe02hH\">Breadth-first numbering: Lessons from a small exercise in algorithm design (Functional Pearl)<\/a>. ~ C. Okasaki #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1G4qKn2\">Budget imbalance criteria for auctions: A formalized theorem<\/a>. ~ M.B. Caminati, M. Kerber &amp; C. Rowat #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1qKjIyy\">Building embedded systems with embedded DSLs<\/a>. ~ P. Hickey et als. #Haskell #Autopilot #Ivory<\/li>\n<li><a href=\"http:\/\/bit.ly\/1E3fqpN\">Category theory for computing science<\/a>. ~ M. Barr &amp; C. Wells #eBook #Logic #CompSci<\/li>\n<li><a href=\"http:\/\/bit.ly\/1EvUjeU\">Certification of confluence proofs using CeTA<\/a>. ~ J. Nagele &amp; R. Thiemann #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1DlXHwr\">Certified Kruskal&#8217;s tree theorem<\/a>. ~ C. Sternagel #ITP #Isabelle_HOL #JFR<\/li>\n<li><a href=\"http:\/\/bit.ly\/V0EuMX\">Certified normalization of context-free grammars<\/a>. ~ D. Firsov &amp; T. Uustalu #ITP #Agda<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ClNWvr\">Certified proof search for intuitionistic linear logic<\/a>. ~ G. Allais &amp; C. McBride #ITP #Agda<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GeKZ59\">Chasing sound, efficient proof with a monadic, HOL system<\/a>. ~ E. Austin &amp; P. Alexander #Logic #Haskell #HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Ajdczh\">Combining proofs and programs in a dependently typed language<\/a>. ~ C. Casinghino, V. Sj\u00f6berg &amp; S. Weirich #Coq <\/li>\n<li><a href=\"http:\/\/bit.ly\/1qgbC1e\">Compiler verification meets cross-language linking via data abstraction<\/a>. ~ P. Wang, S. Cuellar &amp; A. Chlipala #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1lvncmO\">Completeness and decidability results for CTL in Coq<\/a>. ~ C. Doczkal &amp; G. Smolka #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1vBAIul\">Computing with Catalan families, generically<\/a>. ~ P. Tarau #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1wjrFsc\">Conjugate hylomorphisms (Or: the mother of all structured recursion schemes<\/a>) ~ R. Hinze, N. Wu &amp; J. Gibbons #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ckVKVW\">Context-free language theory formalization<\/a>. ~ M.V. Midena #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Q0Pzn9\">Coq as a Metatheory for Nuprl with Bar Induction<\/a>. ~ V. Rahli &amp; M. Bickford #Coq #Nuprl<\/li>\n<li><a href=\"http:\/\/bit.ly\/1JZc7nZ\">Correctness of Isabelle\u2019s cyclicity checker (Implementability of overloading in proof assistants)<\/a>. ~ O. Kuncar #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1yZlJMk\">Declarative game programming (Distilled tutorial)<\/a>. ~ H. Nilsson &amp; I. Perez #FRP #Haskell #Games<\/li>\n<li><a href=\"http:\/\/bit.ly\/1AvrC1J\">Dependently typed programming in Agda<\/a>. ~ U. Norell &amp; J. Chapman #Agda<\/li>\n<li><a href=\"http:\/\/bit.ly\/1zpBLiI\">Depth-first search and strong connectivity in Coq<\/a>. ~ F. Pottier #Coq <\/li>\n<li><a href=\"http:\/\/bit.ly\/1ycMbAb\">Des preuves formelles en Coq du th\u00e9or\u00e8me de Thal\u00e8s pour les cercles<\/a>. ~ D. Braun &amp; N. Magaud #ITP #Coq <\/li>\n<li><a href=\"http:\/\/bit.ly\/1bj9SPB\">Diagnosing Haskell type errors<\/a>. ~ S. Peyton-Jones et als. #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1AfUZI0\">Digital circuits in C\u03bbaSH (Functional specifications and type-directed synthesis)<\/a>. ~ C.P.R. Baaij #PhD_thesis #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ycNfnG\">Double WP : Vers une preuve automatique d&#8217;un compilateur<\/a>. ~ M. Clochard &amp; L. Gondelman #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1MjFMcx\">Echelon form in Isabelle\/HOL<\/a>. ~ J. Divas\u00f3n &amp; J. Aransay #ITP #Isabelle_HOL #AFP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ptqxlA\">Effect capabilities for Haskell<\/a>. ~ I. Figueroa, N. Tabareau &amp; \u00c9. Tanter #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1o1Mo2U\">Effect handlers in scope<\/a>. ~ N. Wu, T. Schrijvers &amp; R. Hinze. #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1LxM3Qs\">Effects, asynchrony, and choice in arrowized functional reactive programming<\/a>. ~ D. Winograd-Cort #PhD_Thesis #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1r6ifDb\">Embedding effect systems in Haskell<\/a>. ~ D. Orchard &amp; T. Petricek #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1y3Trzd\">Embedding of quantified modal logic in higher order logic<\/a>. ~ A. Steen #ITP #Isabelle_HOL <\/li>\n<li><a href=\"http:\/\/bit.ly\/1GtpFYk\">Evaluation of splittable pseudo-random generators<\/a>. ~ H.G. Schaathun #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1qTvlTp\">Exercises on functional programming for domain-specific languages<\/a>. ~ J. Gibbons #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1A1LXgw\">Extensible proof engineering in intensional type theory<\/a>. ~ G. Malecha #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/11FnWgK\">Fiat: Deductive synthesis of abstract data types in a proof assistant<\/a>. ~ B. Delaware et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1JZqPLC\">Fibonacci numbers and the Stern-Brocot tree in Coq<\/a>. ~ J. Grimm #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/bit.ly\/1vlKjPT\">Fixed precision patterns for the formal verification of mathematical constant approximations<\/a>. ~ Y. Bertot #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1phUkRw\">Folding domain-specific languages: Deep and shallow embeddings (Functional pearl)<\/a>. ~ J. Gibbons &amp; N. Wu #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/135lMaS\">Formal analysis of security models for mobile devices, virtualization platforms, and domain name systems<\/a>. ~ C. Luna #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GcJXqy\">Formal kinematic analysis of a general 6R manipulator using the screw theory<\/a>. ~ Aixuan Wu et als. #HOL4<\/li>\n<li><a href=\"http:\/\/bit.ly\/1COfsmT\">Formal proofs for global optimization (Templates and sums of square)<\/a>. ~ V. Magron #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/15HUWam\">Formal proofs for nonlinear optimization<\/a>. ~ V. Magron, X. Allamigeon, S. Gaubert &amp; B. Werner #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1EvN46I\">Formal proofs of rounding error bounds (With application to an automatic positive definiteness check)<\/a>. ~ P. Roux #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1oAlvU3\">Formal specification and verification of computer algebra software<\/a>. ~ M.T. Khan #PhD_Thesis #Why3 #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1BRfexe\">Formal verification for ASP: A case study using the PVS theorem prover<\/a>. ~ F. Aguado et als. #ITP #PVS #ASP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1IUuARq\">Formal verification of Robertson-type uncertainty relation<\/a>. ~ T. Masuhara et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ykta0k\">Formalised set theory: Well-orderings and the axiom of choice<\/a>. ~ D. Kirst #ITP #Coq <\/li>\n<li><a href=\"http:\/\/bit.ly\/1IcXyNs\">Formalising the completeness theorem of classical propositional logic in Agda (Proof pearl)<\/a>. ~ L. Cai et als. #ITP #Agda #Logic<\/li>\n<li><a href=\"http:\/\/bit.ly\/1rX9Xug\">Formalization of Shannon\u2019s theorems<\/a>. ~ R. Affeldt, M. Hagiwara &amp; J. S\u00e9nizergues #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1QHIbCw\">Formalization of closure properties for context-free grammars<\/a>. ~ M.V. M. Ramos &amp; R.J.G.B. de Queiroz #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1xF5kqv\">Formalization of function matrix theory in HOL<\/a>. ~ Z. Shi et als. #ITP #HOL4<\/li>\n<li><a href=\"http:\/\/bit.ly\/16Ptl83\">Formalization of name-stamp protocols<\/a>. ~ T.M.F. Ramos &amp; M. Ayala-Rinc\u00f3n #PVS<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ed22bQ\">Formalization of non-abelian topology for Homotopy Type Theory<\/a>. ~ J.v. Raumer #HoTT #ITP #Lean<\/li>\n<li><a href=\"http:\/\/bit.ly\/1vWFtL9\">Formalization of refinement calculus for reactive systems<\/a>. ~ V. Preoteasa #ITP #Isabelle_HOL #AFP<\/li>\n<li><a href=\"http:\/\/bit.ly\/135i9Sm\">Formalization of statistical conditional independence relations using Coq\/SSReflect<\/a>. ~ J. Wang et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1rrHHiB\">Formalized linear algebra over elementary divisor rings in Coq<\/a>. ~ G. Cano et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/16PvrVF\">Formalizing C in Coq<\/a>. ~ R. Krebbers #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1swIJ2T\">Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective<\/a>. ~ N. Magaud et als. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/bit.ly\/1FEUHIe\">Formalizing alternating-time temporal logic in the Coq proof assistant<\/a>. ~ C. Luna, L. Sierra &amp; D. Zanarini #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1eeTReu\">Formalizing bialgebraic semantics in PVS 6.0<\/a>. ~ S. Smetsers et als. #ITP #PVS<\/li>\n<li><a href=\"http:\/\/bit.ly\/1uVmlPb\">Formalizing complex plane geometry<\/a>. ~ F. Maric &amp; D. Petrovic #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1uUsUz4\">Formalizing provable anonymity in Isabelle\/HOL<\/a>. ~ Y. Li &amp; J. Pang #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/15FHyUA\">Formalizing refinements and constructive algebra in type theory<\/a>. ~ A. M\u00f6rtberg #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/YA8ZuE\">Formalizing semantics with an automatic program verifier<\/a>. ~ M. Clochard et als. #Why3<\/li>\n<li><a href=\"http:\/\/bit.ly\/1LxMwlr\">Formalizing size-optimal sorting networks: Extracting a certified proof checker<\/a>. ~ L. Cruz-Filipe &amp; P. Schneider-Kamp #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1LycST3\">Formally proving a compiler transformation safe<\/a>. ~ J. Breitner http:\/\/bit.ly\/1Lyd1Wt #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GcLnRR\">Formally verified analysis of resource sharing conflicts in multithreaded Java<\/a>. ~ N. Baklanova #PhD_Thesis #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1y3hnTL\">Formally verified computation of enclosures of solutions of ordinary differential equations<\/a>. ~ F. Immler #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1wPAnkh\">Formally verified modular semantics<\/a>. ~ K. Madlener #PhD_Thesis  #ITP #Coq #PVS<\/li>\n<li><a href=\"http:\/\/bit.ly\/1PXZZDR\">Formally verifying transfer functions of analog circuits using theorem proving<\/a>. ~ S.H. Taqdees &amp; O. Hasan #HOL_Light<\/li>\n<li><a href=\"http:\/\/1.usa.gov\/1ubjDYk\">Formally-verified decision procedures for univariate polynomial computation based on Sturm\u2019s and Tarski\u2019s theorems<\/a>. ~ C. Mu\u00f1oz #PVS<\/li>\n<li><a href=\"http:\/\/bit.ly\/1J89QXC\">Foundational extensible corecursion: a proof assistant perspective<\/a>. ~ J. Blanchette, A. Popescu &amp; D. Traytel #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1A1xouZ\">Functional Pearl 1: The min missing natural number<\/a>. ~ Jackson Tale #Algorithmic #FP #OCaml <\/li>\n<li><a href=\"http:\/\/bit.ly\/1sJC8zm\">Functional Pearl: A program to solve Sudoku<\/a>. ~ R. Bird #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Ctb7Ut\">Functional Pearl: Deletion (The curse of the red-black tree)<\/a>. ~ K. Germane &amp; M. Might #Racket #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1BRfZq6\">Functional Reactive Programming and its application in Functional Game Programming<\/a>. ~ D. Kraeutmann &amp; P. Kindermann #FRP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1r7EqnC\">Functional pearl: The decorator pattern in Haskell<\/a>. ~ N. Collins &amp; T. Sheard #Haskell #Python<\/li>\n<li><a href=\"http:\/\/bit.ly\/1uTbsyd\">Functional pearl: finding a densest segment<\/a>. ~ Sharon Curtis &amp; Shin-Cheng Mu #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1tz5FOY\">Functional programming with bananas, lenses, envelopes and barbed wire<\/a>. ~ E. Meijer, M. Fokkinga &amp; R. Paterson #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/WbPDLx\">Gauss-Jordan algorithm and its applications<\/a>. ~ J. Divas\u00f3n &amp; J. Aransay #ITP #AFP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1F4Etws\">Generalizing a mathematical analysis library in Isabelle\/HOL<\/a>. ~ J. Aransay &amp; J. Divas\u00f3n #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1FgWm5T\">Getting a quick fix on comonads<\/a>. ~ K. Foner #Logic #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GcHJYc\">Gradual certified programming in Coq<\/a>. ~ T. Eric &amp; N. Tabareau #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1wjGH1e\">Graphes et couplages en Coq<\/a>. ~ C. Dubois et als. #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1pF35VQ\">HERMIT: An Equational Reasoning Model to Implementation Rewrite System for Haskell<\/a>. ~ A. Gill #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1zpCssk\">HOCore in Coq<\/a>. ~ M. Escarr\u00e1, P. Maksimovi\u0107 &amp; A. Schmitt #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1KRsQdC\">Hermite normal form in Isabelle\/HOL<\/a>. ~  J. Divas\u00f3n &amp; J. Aransay #ITP #Isabelle_HOL #AFP<\/li>\n<li><a href=\"http:\/\/bit.ly\/SQkETm\">Higher-order automated theorem provers<\/a>. ~ C. Benzm\u00fcller #ITP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1q1fLEN\">Hindley-Milner elaboration in applicative style (Functional pearl)<\/a>. ~ F. Pottier #OCaml<\/li>\n<li><a href=\"http:\/\/bit.ly\/1zFD7Ww\">Homotopy type theory: Unified foundations of mathematics and computation<\/a>. ~ S. Awodey &amp; R. Harper #HoTT #Math #CompSci <\/li>\n<li><a href=\"http:\/\/bit.ly\/1sZL5Rg\">Homotopy type theory<\/a>. ~ A. Pelayo &amp; M.A. Warren #HoTT<\/li>\n<li><a href=\"http:\/\/bit.ly\/1koBfuU\">Hot code reloading in Cloud Haskell<\/a>. ~ Pankaj More #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1FgVy0R\">How to express convergence for analysis in Coq<\/a>. ~ C. Lelay #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1NRPSRT\">Hygame: Teaching Haskell using games<\/a>. ~ Z. Baharav &amp; D.S. Gladstein #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Ed3SUm\">Idris: A functional programming language with dependent types<\/a>. ~ F. Teegen #Idris<\/li>\n<li><a href=\"http:\/\/bit.ly\/1qAPqce\">Imperative insertion sort in Isabelle\/HOL<\/a>. ~ C. Sternagel #AFP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1DlZCku\">Innocuous double rounding of basic arithmetic operations<\/a>. ~ P. Roux #ITP #Coq #JFR <\/li>\n<li><a href=\"http:\/\/bit.ly\/1EHL3ZD\">Interacting with modal logics in the Coq proof assistant<\/a>. ~ C. Benzm\u00fcller &amp; B. Woltzenlogel Paleo #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1cdFner\">Intermediate Logic<\/a>. ~ R. Zach #eBook #Logic<\/li>\n<li><a href=\"http:\/\/bit.ly\/1nkCZGH\">Introducing functional programmers to interactive theorem proving and program verification<\/a>. ~ I. Sergey &amp; A. Nanevski #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1rgRX1m\">Introduction to computational logic<\/a>. ~ G. Smolka &amp; C.E. Brown #eBook #Logic #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ClM8mc\">Isabelle and security<\/a>. ~ J.C. Blanchette &amp; A. Popescu #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1qemF8H\">Krivine nets: A semantic foundation for distributed execution<\/a>. ~ O. Fredriksson &amp; D.R. Ghica #Agda<\/li>\n<li><a href=\"http:\/\/bit.ly\/Zz6YQV\">Lattice-based data structures for deterministic parallel and distributed programming<\/a>. ~ L. Kuper @lindsey #PdD_Thesis #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1MAp9aX\">Layers, resources and property templates in the specification and analysis of two interactive systems<\/a>. ~ J.C. Campos #ITP #PVS<\/li>\n<li><a href=\"http:\/\/bit.ly\/1qYRS3p\">Learn Physics by programming in Haskell<\/a>. ~ S.N. Walck #Haskell <\/li>\n<li><a href=\"http:\/\/bit.ly\/1AfW8PA\">Learning-based relevance filter for Isabelle\/HOL<\/a>. ~ J.C. Blanchette et als. #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GjIich\">Lenses in functional programming<\/a>. ~ A. Steckermeier #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Q8V2Lk\">Lightweight higher-order rewriting in Haskell<\/a>. ~ E. Axelsson &amp; A. Vezzosi #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1pF0HhY\">LiquidHaskell: Experience with refinement types in the real World<\/a>. ~ N. Vazou, E.L. Seidel &amp; R. Jhala #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GeNHaP\">LiquidHaskell: Refinement types in the real world<\/a>. ~ N. Vazou, E.L. Seidel &amp; R. Jhala #Haskell #SMT<\/li>\n<li><a href=\"http:\/\/bit.ly\/1wZgcRF\">Logic and computation<\/a>. ~ B. Pientka #eBook #Logic #CompSci<\/li>\n<li><a href=\"http:\/\/bit.ly\/1vLkXhA\">Logic for problem solving, revisited<\/a>. ~ Robert Kowalski #eBook #Logic #CompSci #LP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1A2LV6x\">Machine-checked proofs for realizability checking algorithms<\/a>. ~ A. Katis, A. Gacek, M.W. Whalen #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1F4FBQR\">Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation<\/a>. ~ #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Axs7bb\">Maximally permissive controlled system synthesis for modal logic<\/a>. ~ A.C. van Hulst, M.A. Reniers &amp; W.J. Fokkink #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1qzVBAP\">Mechanized network origin and path authenticity proofs<\/a>&#8211; ~ F. Zhang et als. #Coq <\/li>\n<li><a href=\"http:\/\/bit.ly\/1DuWDoW\">Mechanized support for the formal especification, verification and deployment of component-based applications<\/a>. ~ N. Gaspar #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1zISHOM\">Mechanized verification of fine-grained concurrent programs<\/a>. ~ I. Sergey, A. Nanevski &amp; A. Banerjee #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Kn4iHB\">Mining the Archive of Formal Proofs<\/a>. ~ J.C. Blanchette, M. Haslbeck, D. Matichuk &amp; T. Nipkow #Isabelle_HOL #AFP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1u5gXIV\">Modeling human behaviour with Higher Order Logic: insider threats<\/a>. ~ J. Boender #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1quOeNn\">Modeling set theory in homotopy type theory<\/a>. ~ J\u00e9r\u00e9my Ledent #HoTT #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1xD2vaU\">Modelling algebraic structures and morphisms in ACL2<\/a>. ~ J. Heras, F.J. Mart\u00edn &amp; V. Pascual. #ITP #ACL2<\/li>\n<li><a href=\"http:\/\/bit.ly\/1JkjEfI\">Mutual exclusion by four shared bits with not more than quadratic complexity<\/a>. ~ W.H. Hesselink #ITP #PVS <\/li>\n<li><a href=\"http:\/\/bit.ly\/1FgUUR9\">Natural language reasoning using Coq: interaction and automation<\/a>. ~ S. Chatzikyriakidis #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1umxx8c\">New arithmetic algorithms for hereditarily binary natural numbers<\/a>. ~ P. Tarau #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1fFRliH\">Numerical mathematics on FPGAs using C\u03bbaSH<\/a>. ~ M. Bakker #Haskell #Math<\/li>\n<li><a href=\"http:\/\/bit.ly\/1yUlGMB\">Object-oriented style overloading for Haskell<\/a>. ~ M. Shields &amp; S. Peyton Jones #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1fswTBx\">On Euclid&#8217;s algorithm and elementary number theory<\/a>. ~ R. Backhouse &amp; J.F. Ferreira #Algorithms<\/li>\n<li><a href=\"http:\/\/bit.ly\/1t5sJlX\">On the formalization of signal-flow-graphs in HOL<\/a>. ~ S.M. Beillahi, U. Siddique &amp; S. Tahar #ITP #HOL_Light <\/li>\n<li><a href=\"http:\/\/bit.ly\/TJYsLA\">Optimising embedded domain specific languages (eDSL) using template Haskell<\/a>. ~ L.J. Buit #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1uEWYQu\">Optimising purely functional GPU programs<\/a>. ~ T.L. McDonell #PhD_Thesis #Haskell <\/li>\n<li><a href=\"http:\/\/bit.ly\/1BcB7Aj\">Parsing parses: A pearl of (dependently typed) programming and proof<\/a>. ~ J. Gross &amp; A. Chlipala #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1jaMztH\">Picat: A Logic-based multi-paradigm language<\/a>. ~ H. Kjellerstrand #LP #FP #Picat #Prolog<\/li>\n<li><a href=\"http:\/\/bit.ly\/1oGyKUM\">Pointer program derivation using Coq: Graphs and Schorr-Waite algorithm<\/a>. ~ J.F. Dufourd #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1eeSahf\">Practical principled FRP (Forget the past, change the future, FRPNow!<\/a>) ~ A. van der Ploeg &amp; K. Claessen #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/12ooEiF\">Principles for verification tools: Separation logic<\/a>. ~ B. Dongol, V.B.F. Gomes &amp; G. Struth #ITP #Isabelle_HOL <\/li>\n<li><a href=\"http:\/\/bit.ly\/1umppVo\">Priorities without priorities: Representing preemption in psi-calculi<\/a>. ~ J.A. Pohjola &amp; J. Parrow #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1CsByra\">Program verification by coinduction<\/a>. ~ B. Moore &amp; G. Rosu #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GpwJ8y\">Programming with refinement types: An introduction to LiquidHaskell<\/a>. ~ R. Jhala et als. #eBook #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1tdu8ES\">Programs and proofs (Mechanizing mathematics with dependent types)<\/a>. ~ I. Sergey #eBook #ITP #Coq <\/li>\n<li><a href=\"http:\/\/bit.ly\/1o1MGqy\">Promoting functions to type families in Haskell<\/a>. ~ R.A. Eisenberg &amp; J. Stolarek. #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GI4S2P\">Propositional calculus in Coq<\/a>. ~ F.v. Doorn #Logic #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1tB3uV4\">Proving tight bounds on univariate expressions in Coq<\/a>. ~ \u00c9. Martin-Dorel &amp; G. Melquiond #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1Erbz63\">QR decomposition in Isabelle\/HOL<\/a>. ~ J. Divas\u00f3n &amp; J. Aransay #ITP  #Isabelle_HOL #AFP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1rpCgE2\">QuickChick: A Coq framework for verified property-based testing<\/a>. ~ Z. Paraskevopoulou &amp; C. Hritcu #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1rMF7ZH\">Real-valued special functions: upper and lower bounds<\/a>. ~ L.C. Paulson #ITP #AFP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ed0azG\">Reasoning with the HERMIT (Tool support for equational reasoning on GHC core programs)<\/a>. ~ A. Farmer, N. Sculthorpe &amp; A. Gill #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1LxMV7E\">Refinement to certify abstract interpretations, illustrated on linearization for polyhedra<\/a>. ~ S. Boulm\u00e9 &amp; A. Mar\u00e9chal #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1lfv8Td\">Refinement types For Haskell<\/a>. ~ N. Vazou et als. #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1DlWqFM\">Relative monads formalised<\/a>. ~ T. Altenkirch, J. Chapman &amp; T. Uustalu #Agda #JFR<\/li>\n<li><a href=\"http:\/\/bit.ly\/1dc2i9M\">Relativistic programming in Haskell (Using types to enforce a critical section discipline)<\/a>. ~ T. Cooper &amp; J. Walpole #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1psomBr\">Representing game dialogue as expressions in first-order logic<\/a>. ~ K. Wheeler #Logic #NLP #Clojure<\/li>\n<li><a href=\"http:\/\/bit.ly\/1D4TaJt\">Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions<\/a>. ~ A. Solovyev #HOL_Light<\/li>\n<li><a href=\"http:\/\/bit.ly\/1qKhShj\">Safe zero-cost coercions for Haskell<\/a>. ~ J. Breitner et als. #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1tz604s\">Scrap your boilerplate with class: extensible generic functions<\/a>. ~ R. L\u00e4mmel &amp; Simon Peyton Jones. #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1w87S59\">Security type systems and deduction<\/a>. ~ T. Nipkow &amp; A. Popescu #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1NxMIAD\">Semantics for programming languages with Coq encodings<\/a>. ~ Y. Bertot #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1kU6cap\">Semantics of intuitionistic propositional logic: Heyting algebras and Kripke models<\/a>. ~ C.E. Brown #Logic #ITP #Coq <\/li>\n<li><a href=\"http:\/\/bit.ly\/1nKyAHT\">Sets, the axiom of choice, and all that: A tutorial<\/a>. ~ E.E. Doberkat #Math #Logic #CompSci<\/li>\n<li><a href=\"http:\/\/bit.ly\/1AoiTPD\">Simple balanced binary search trees<\/a>. ~ P. Ragde #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1pE5PQa\">SmartCheck: Automatic and efficient counterexample reduction and generalization<\/a>. ~ Lee Pike #Haskell<\/li>\n<li><a href=\"http:\/\/1.usa.gov\/1MAoSVj\">Software validation via model animation<\/a>. ~ A.M. Dutle, C.A. Mu\u00f1oz, A.J. Narkawicz &amp; R.W. Butler #ITP #PVS<\/li>\n<li><a href=\"http:\/\/bit.ly\/1tGE37x\">Some lessons learned on writing predicate logic proofs in Isabelle\/Isar<\/a>. ~ W. Schreiner #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ClN5e9\">Specifying and verifying IP with linear logic<\/a>. ~ D. Sinclair et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1syuicH\">Stream fusion in HOL with code generation<\/a>. ~ A. Lochbihler #ITP #Isabelle_HOL #AFP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1zTRkQ7\">Structures alg\u00e9briques et programmation<\/a>. ~ G. Connan. #eBook #Math #Haskell <\/li>\n<li><a href=\"http:\/\/bit.ly\/1pEZOGb\">Suitability of Haskell for multi-agent systems<\/a>. ~ T. de Jong #Hakell #MAS<\/li>\n<li><a href=\"http:\/\/bit.ly\/1HTxrwY\">Systematic verification of the modal logic cube in Isabelle\/HOL<\/a>. ~ C. Benzm\u00fcller &amp; M. Claus #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1G9IQRM\">Teaching Logic to Information Systems students: Challenges and opportunities<\/a>. ~ A. Zamansky &amp; E. Farchi #Logic<\/li>\n<li><a href=\"http:\/\/bit.ly\/1uVb9SH\">Teaching students property-based testing<\/a>. ~ Clara Benac Earle et als. #FP #Erlang #QuickCheck<\/li>\n<li><a href=\"http:\/\/bit.ly\/1szJcOi\">Termination with domain theory<\/a>. ~ J. Oberhauser #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1u9KGyB\">The CAVA automata library<\/a>. ~ P. Lammich #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1oTZM7u\">The Cayley-Hamilton theorem in Isabelle\/HOL<\/a>. ~ S. Adelsberger &amp; S. Hetzl #ITP #Isabelle_HOL #AFP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1vxIWo9\">The Gilbreath trick: A case study in axiomatisation and proof development in the Coq proof assistant<\/a>. ~ G. Huet (1991) #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/YBXxjj\">The Jordan-H\u00f6lder theorem in Isabelle\/HOL<\/a>. ~ J. von Raumer #AFP #Isabelle\/HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1yksQ1y\">The Sturm-Tarski theorem in Isabelle\/HOL<\/a>. ~ W. Li #AFP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1z6QhI9\">The Unified Policy Framework (UPF)<\/a>. ~ A.D. Brucker, L. Br\u00fcgger &amp; B. Wolff #ITP #Isabell_HOL <\/li>\n<li><a href=\"http:\/\/bit.ly\/1wOFyWn\">The arithmetic of even-odd trees<\/a>. ~ Paul Tarau #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1PyNyQx\">The essence of the iterator pattern<\/a>. ~ J. Gibbons &amp; B.C.d.S. Oliveira #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1JMFpWf\">The formalization of discrete Fourier transform in HOL<\/a>. ~ Z. Shi et als. #ITP #HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1szIRel\">The foundational cryptography framework<\/a>. ~ A. Petcher &amp; G. Morrisett #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1FmxOZY\">The maximum segment sum problem: Its origin, and a derivation<\/a>. ~ Shin-Cheng Mu #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1GmvC4O\">The proof is in the plugin<\/a>. ~ E. Austin &amp; P. Alexander #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1jwb6Uy\">The proof is in the process. A preamble for a philosophy of computer-assisted mathematics<\/a>. ~ L. de Mol #ITP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1CiZQGL\">The selection monad as a CPS translation<\/a>. ~ J. Hedges #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1qKiSSD\">There is no fork: an abstraction for efficient, concurrent, and concise data access<\/a>. ~ S. Marlow et als. #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1KmPuvG\">Thinking with laziness<\/a>. ~ T. Jelvis #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1xIn7U4\">Towards a theory of reach<\/a>. ~ J. Fowler &amp; G. Hutton #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1EvNF8r\">Towards formal fault tree analysis using theorem proving<\/a>. ~ W. Ahmed &amp; O. Hasan #HOL4 #ITP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1A5XT32\">Towards the formalization of fractional calculus in Higher-Order Logic<\/a>. ~ U. Siddique, O. Hasan &amp; S. Tahar #ITP #HOL_Light<\/li>\n<li><a href=\"http:\/\/bit.ly\/15jsKLp\">Tutorial on LiquidHaskell<\/a>. ~ N. Vazou, E. Seidel, P. Rondon, and R. Jhala #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1MAprP3\">Two axiomatizations of Nelson algebras<\/a>. ~ A. Grabowski #ITP #Mizar<\/li>\n<li><a href=\"http:\/\/bit.ly\/1JF0kgs\">Two can keep a secret, if one of them uses Haskell (Functional pearl)<\/a>. ~ A. Russo #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1B52nmZ\">Typed faceted values for secure information flow in Haskell<\/a>. ~ T.H. Austin, K. Knowles &amp; C. Flanagan #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1qLTVBm\">Un ordinateur pour v\u00e9rifier les preuves math\u00e9matiques<\/a>. ~ Assia Mahboubi #Math #CompSci #ITP<\/li>\n<li><a href=\"http:\/\/bit.ly\/1nqjWWd\">Upon the Haskell support for the web applications development<\/a>. ~ A. Vasilescu #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1ISBd9w\">Validating dominator trees for a fast, verified dominance test<\/a>. ~ S. Blazy, D. Demange &amp; D. Pichardie #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/WbQXhG\">Vector spaces (formalisation of basic linear algebra)<\/a>. ~ H. Lee #ITP #AFP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/16PuEUo\">Verification of Faust (Functional Audio Stream) signal processing programs in Coq<\/a>. ~ E.J. Gallego, O. Hermant &amp; P. Jouvelot #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1zGCjh9\">Verification of a cryptographic primitive: SHA-256<\/a>. ~ A.W. Appel #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1LxKP7R\">Verification of system FC in Coq<\/a>. ~ T. Garsyset als. #Coq #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1KJjKh1\">Verified correctness and security of OpenSSL HMAC<\/a>. ~ L. Beringer, A. Petcher, K.Q. Ye @hypotext &amp; A.W. Appel #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1jwadvn\">Verified efficient implementation of Gabow\u2019s strongly connected component algorithm<\/a>. ~ P. Lammich #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1oV9XNI\">Verified functional programming in Agda<\/a>. ~ A. Stump #eBook #FP #Agda<\/li>\n<li><a href=\"http:\/\/bit.ly\/135k0q8\">Verified generation of glue code for ROS-based control systems<\/a>. ~ W. Meng et als. #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/184UCn0\">Verified reachability analysis of continuous systems<\/a>. ~ F. Immler #ITP #Isabelle_HOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/1wRERve\">Verified validation of program slicing<\/a>. ~ S. Blazy et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1AfWpCi\">Verifying fast and sparse SSA-based optimizations in Coq<\/a>. ~ D. Demange #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1dc2Lce\">Verifying type class laws with equational reasoning<\/a>. ~ L. Hofmaier #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1FXCzwn\">Views of PI: Definition and computation<\/a>. ~ Y. Bertot &amp; G. Allais #ITP #Coq<\/li>\n<li><a href=\"http:\/\/bit.ly\/1sYYFET\">Visualisation of Haskell performance<\/a>. ~ Peter Moritz Wortmann #PhD_Thesis #Haskell <\/li>\n<li><a href=\"http:\/\/bit.ly\/1MAndPK\">Vote counting as mathematical proof<\/a>. ~ D. Pattinson #ITP #Coq #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/1lfpXmm\">Worker\/wrapper\/makes it\/faster<\/a>. ~ J. Hackett &amp; G. Hutton. #Haskell <\/li>\n<li><a href=\"http:\/\/bit.ly\/1eeU5lZ\">Zippers and data type derivatives<\/a>. ~ S. Ro\u00dfkopf #Haskell<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas este curso (del 29 de junio de 2014 al 15 de julio de 2015) en Twitter sobre l\u00f3gica computacional y programaci\u00f3n funcional. Al final de cada art\u00edculo se encuentra etiquetas relativas a los sistemas que usa o a su contenido. A Coq formalization of a sign determination&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[6,177],"tags":[292],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4945"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4945"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4945\/revisions"}],"predecessor-version":[{"id":4946,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4945\/revisions\/4946"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4945"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4945"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4945"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}