Lecturas

Esta entrada es una recopilación de lecturas compartidas este curso (del 29 de junio de 2014 al 15 de julio de 2015) en
Twitter sobre lógica computacional y programación funcional.

Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

• A Coq formalization of a sign determination algorithm in real algebraic geometry. ~ C. Cohen & M. Kohli #Coq
• A Haskell implementation of a rule-based program transformation for C programs. ~ S. Tamarit et als. #Haskell
• A Haskell monad for infinite search in finite time. ~ M. Escardo #Haskell
• A combinator library for MCMC sampling. ~ P. Narayanan & C.C. Shan #Haskell
• A concrete deskolemization algorithm. ~ R. van Sparrentak #Logic #Haskell
• A constructive semantics for rewriting logic. ~ M.N. Kaplan #ITP #Coq
• A course in Haskell-based software testing. ~ J. van Eijck & V. Zaytsev #Haskell
• A formal and constructive theory of computation. ~ Y. Forster #Coq
• A formal proof of the Kepler conjecture. ~ T. Hales et als. #ITP #HOL_LIght #Isabelle_HOL
• A formal verification of the theory of parity complexes. ~ M. Buckley #Coq
• A formalisation of Sturm’s theorem. ~ M. Eberl #ITP #Isabelle_HOL
• A formalisation of finite automata using hereditarily finite sets. ~ L.C. Paulson #ITP #Isabelle_HOL
• A formalization in Coq of Edwardk Kmett’s Hask library for Haskell. ~ J. Wiegley & E. Kmett #ITP #Coq #Haskell
• A formalization of strand spaces in Coq. ~ Hai Nguyen #ITP #Coq
• A formalized hierarchy of probabilistic system types. ~ J. Hölzl, A. Lochbihler & D. Traytel #Isabelle_HOL #ITP
• A formally-verified C static analyzer. ~ J.H. Jourdan et als. #ITP #Coq
• A formally-verified decision procedure for univariate polynomial computation based on Sturm’s Theorem. ~ C. Muñoz et al. #PVS
• A framework for developing stand-alone certifiers. ~ C. Sternagel & R. Thiemann #Isabelle_HOL
• A framework for exploring finite models. ~ S. Saghafi #PhD_Thesis #Logic #Haskell
• A framework for verified depth-first algorithms. ~ R. Neumann #ITP #Isabelle_HOL
• A generic numbering system based on Catalan families of combinatorial objects. ~ P. Tarau #Haskell
• A mechanisation of internal Galois connections in order theory formalised without meets. ~ M. Al-Hassy #Agda
• A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. ~ L.C. Paulson #ITP #Isabelle_HOL
• A mechanized verification environment for real-time process algebras and low-level programming languages. ~ B. Bartels #Thesis #ITP #Isabelle_HOL
• A nominal exploration of intuitionism. ~ V. Rahli & M. Bickford #ITP #Nuprl
• A pilot study of the use of LogEx, lessons learned. ~ J. Lodder, B. Heeren & J. Jeuring #Logic
• A primer on Homotopy Type Theory (Part 1: The formal type theory). ~ J. Ladyman & S. Presnell #HoTT
• A semantics for intuitionistic higher-order logic supporting higher-order abstract syntax. ~ C.E. Brown #Logic #ITP #Coq
• A typechecker plugin for units of measure (Domain-specific constraint solving in GHC Haskell). ~ A. Gundry #Haskell
• A typed C11 semantics for interactive theorem proving. ~ R. Krebbers & F. Wiedijk #ITP #Coq
• A verified enclosure for the Lorenz attractor (Rough diamond). ~ F. Immler #ITP #Isabelle_HOL
• Affine arithmetic. ~ F. Immler #ITP #Isabelle_HOL
• Amortized complexity verified. ~ T. Nipkow #ITP #Isabelle_HOL
• An intrinsic encoding of a subset of C and its application to TLS network packet processing. ~ R. Affeldt & K. Sakaguchi #Coq
• An introduction to proof assistants. ~ P. Schnider #ITP
• An investigation into the use of Haskell for dynamic programming. ~ D. McGillicuddy, A.J. Parkes & H. Nilsson #Haskell
• An overabundance of equality: Implementing kind equalities into Haskell. ~ R.A. Eisenberg #Haskell
• Applicative bidirectional programming with lenses. ~ K. Matsuda & M. Wang #Haskell
• Au delà des réels: méthodes numériques en informatique. ~ G. Connan #eBook #Math #Haskell
• Automated generation of machine verifiable and readable proofs: A case study of Tarski’s geometry. ~ J. Narboux et als. #Coq
• Automated verification of role-based access control policies constraints using Prover9. ~ K.E. Sabri #ATP #Prover9
• Automatic and transparent transfer of theorems along isomorphisms in the Coq proof assistant. ~ T. Zimmermann & H. Herbelin #Coq
• Automatically verified implementation of data structures based on AVL trees. ~ M. Clochard #Why3
• Automating change of representation for proofs in discrete mathematics. ~ D. Raggi, A. Bundy, G. Grov & A. Pease #Isabelle_HOL
• Automating formal proofs for reactive systems. ~ D. Ricketts et als. #Coq
• Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light. ~ L. Michel #HOL_Light
• Bind induction: Extracting monadic programs from proofs. ~ H. Shafei & J. Caldwell #Haskell #Coq
• Bounded refinement types. ~ N. Vazou, A. Bakst & R. Jhala #Haskell
• Breadth-first numbering: Lessons from a small exercise in algorithm design (Functional Pearl). ~ C. Okasaki #Haskell
• Budget imbalance criteria for auctions: A formalized theorem. ~ M.B. Caminati, M. Kerber & C. Rowat #ITP #Isabelle_HOL
• Building embedded systems with embedded DSLs. ~ P. Hickey et als. #Haskell #Autopilot #Ivory
• Category theory for computing science. ~ M. Barr & C. Wells #eBook #Logic #CompSci
• Certification of confluence proofs using CeTA. ~ J. Nagele & R. Thiemann #Isabelle_HOL
• Certified Kruskal’s tree theorem. ~ C. Sternagel #ITP #Isabelle_HOL #JFR
• Certified normalization of context-free grammars. ~ D. Firsov & T. Uustalu #ITP #Agda
• Certified proof search for intuitionistic linear logic. ~ G. Allais & C. McBride #ITP #Agda
• Chasing sound, efficient proof with a monadic, HOL system. ~ E. Austin & P. Alexander #Logic #Haskell #HOL
• Combining proofs and programs in a dependently typed language. ~ C. Casinghino, V. Sjöberg & S. Weirich #Coq
• Compiler verification meets cross-language linking via data abstraction. ~ P. Wang, S. Cuellar & A. Chlipala #ITP #Coq
• Completeness and decidability results for CTL in Coq. ~ C. Doczkal & G. Smolka #ITP #Coq
• Computing with Catalan families, generically. ~ P. Tarau #Haskell
• Conjugate hylomorphisms (Or: the mother of all structured recursion schemes) ~ R. Hinze, N. Wu & J. Gibbons #Haskell
• Context-free language theory formalization. ~ M.V. Midena #Coq
• Coq as a Metatheory for Nuprl with Bar Induction. ~ V. Rahli & M. Bickford #Coq #Nuprl
• Correctness of Isabelle’s cyclicity checker (Implementability of overloading in proof assistants). ~ O. Kuncar #Isabelle_HOL
• Declarative game programming (Distilled tutorial). ~ H. Nilsson & I. Perez #FRP #Haskell #Games
• Dependently typed programming in Agda. ~ U. Norell & J. Chapman #Agda
• Depth-first search and strong connectivity in Coq. ~ F. Pottier #Coq
• Des preuves formelles en Coq du théorème de Thalès pour les cercles. ~ D. Braun & N. Magaud #ITP #Coq
• Diagnosing Haskell type errors. ~ S. Peyton-Jones et als. #Haskell
• Digital circuits in CλaSH (Functional specifications and type-directed synthesis). ~ C.P.R. Baaij #PhD_thesis #Haskell
• Double WP : Vers une preuve automatique d’un compilateur. ~ M. Clochard & L. Gondelman #Coq
• Echelon form in Isabelle/HOL. ~ J. Divasón & J. Aransay #ITP #Isabelle_HOL #AFP
• Effect capabilities for Haskell. ~ I. Figueroa, N. Tabareau & É. Tanter #Haskell
• Effect handlers in scope. ~ N. Wu, T. Schrijvers & R. Hinze. #Haskell
• Effects, asynchrony, and choice in arrowized functional reactive programming. ~ D. Winograd-Cort #PhD_Thesis #Haskell
• Embedding effect systems in Haskell. ~ D. Orchard & T. Petricek #Haskell
• Embedding of quantified modal logic in higher order logic. ~ A. Steen #ITP #Isabelle_HOL
• Evaluation of splittable pseudo-random generators. ~ H.G. Schaathun #Haskell
• Exercises on functional programming for domain-specific languages. ~ J. Gibbons #Haskell
• Extensible proof engineering in intensional type theory. ~ G. Malecha #PhD_Thesis #ITP #Coq
• Fiat: Deductive synthesis of abstract data types in a proof assistant. ~ B. Delaware et als. #ITP #Coq
• Fibonacci numbers and the Stern-Brocot tree in Coq. ~ J. Grimm #ITP #Coq #Math
• Fixed precision patterns for the formal verification of mathematical constant approximations. ~ Y. Bertot #ITP #Coq
• Folding domain-specific languages: Deep and shallow embeddings (Functional pearl). ~ J. Gibbons & N. Wu #Haskell
• Formal analysis of security models for mobile devices, virtualization platforms, and domain name systems. ~ C. Luna #Coq
• Formal kinematic analysis of a general 6R manipulator using the screw theory. ~ Aixuan Wu et als. #HOL4
• Formal proofs for global optimization (Templates and sums of square). ~ V. Magron #PhD_Thesis #ITP #Coq
• Formal proofs for nonlinear optimization. ~ V. Magron, X. Allamigeon, S. Gaubert & B. Werner #ITP #Coq
• Formal proofs of rounding error bounds (With application to an automatic positive definiteness check). ~ P. Roux #ITP #Coq
• Formal specification and verification of computer algebra software. ~ M.T. Khan #PhD_Thesis #Why3 #Coq
• Formal verification for ASP: A case study using the PVS theorem prover. ~ F. Aguado et als. #ITP #PVS #ASP
• Formal verification of Robertson-type uncertainty relation. ~ T. Masuhara et als. #ITP #Coq
• Formalised set theory: Well-orderings and the axiom of choice. ~ D. Kirst #ITP #Coq
• Formalising the completeness theorem of classical propositional logic in Agda (Proof pearl). ~ L. Cai et als. #ITP #Agda #Logic
• Formalization of Shannon’s theorems. ~ R. Affeldt, M. Hagiwara & J. Sénizergues #ITP #Coq
• Formalization of closure properties for context-free grammars. ~ M.V. M. Ramos & R.J.G.B. de Queiroz #ITP #Coq
• Formalization of function matrix theory in HOL. ~ Z. Shi et als. #ITP #HOL4
• Formalization of name-stamp protocols. ~ T.M.F. Ramos & M. Ayala-Rincón #PVS
• Formalization of non-abelian topology for Homotopy Type Theory. ~ J.v. Raumer #HoTT #ITP #Lean
• Formalization of refinement calculus for reactive systems. ~ V. Preoteasa #ITP #Isabelle_HOL #AFP
• Formalization of statistical conditional independence relations using Coq/SSReflect. ~ J. Wang et als. #ITP #Coq
• Formalized linear algebra over elementary divisor rings in Coq. ~ G. Cano et als. #ITP #Coq
• Formalizing C in Coq. ~ R. Krebbers #Coq
• Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective. ~ N. Magaud et als. #ITP #Coq #Math
• Formalizing alternating-time temporal logic in the Coq proof assistant. ~ C. Luna, L. Sierra & D. Zanarini #ITP #Coq
• Formalizing bialgebraic semantics in PVS 6.0. ~ S. Smetsers et als. #ITP #PVS
• Formalizing complex plane geometry. ~ F. Maric & D. Petrovic #ITP #Isabelle_HOL
• Formalizing provable anonymity in Isabelle/HOL. ~ Y. Li & J. Pang #Isabelle_HOL
• Formalizing refinements and constructive algebra in type theory. ~ A. Mörtberg #PhD_Thesis #ITP #Coq
• Formalizing semantics with an automatic program verifier. ~ M. Clochard et als. #Why3
• Formalizing size-optimal sorting networks: Extracting a certified proof checker. ~ L. Cruz-Filipe & P. Schneider-Kamp #Coq
• Formally proving a compiler transformation safe. ~ J. Breitner http://bit.ly/1Lyd1Wt #ITP #Isabelle_HOL
• Formally verified analysis of resource sharing conflicts in multithreaded Java. ~ N. Baklanova #PhD_Thesis #Isabelle_HOL
• Formally verified computation of enclosures of solutions of ordinary differential equations. ~ F. Immler #Isabelle_HOL
• Formally verified modular semantics. ~ K. Madlener #PhD_Thesis #ITP #Coq #PVS
• Formally verifying transfer functions of analog circuits using theorem proving. ~ S.H. Taqdees & O. Hasan #HOL_Light
• Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems. ~ C. Muñoz #PVS
• Foundational extensible corecursion: a proof assistant perspective. ~ J. Blanchette, A. Popescu & D. Traytel #Isabelle_HOL
• Functional Pearl 1: The min missing natural number. ~ Jackson Tale #Algorithmic #FP #OCaml
• Functional Pearl: A program to solve Sudoku. ~ R. Bird #Haskell
• Functional Pearl: Deletion (The curse of the red-black tree). ~ K. Germane & M. Might #Racket #Haskell
• Functional Reactive Programming and its application in Functional Game Programming. ~ D. Kraeutmann & P. Kindermann #FRP
• Functional pearl: The decorator pattern in Haskell. ~ N. Collins & T. Sheard #Haskell #Python
• Functional pearl: finding a densest segment. ~ Sharon Curtis & Shin-Cheng Mu #Haskell
• Functional programming with bananas, lenses, envelopes and barbed wire. ~ E. Meijer, M. Fokkinga & R. Paterson #Haskell
• Gauss-Jordan algorithm and its applications. ~ J. Divasón & J. Aransay #ITP #AFP #Isabelle_HOL
• Generalizing a mathematical analysis library in Isabelle/HOL. ~ J. Aransay & J. Divasón #ITP #Isabelle_HOL
• Getting a quick fix on comonads. ~ K. Foner #Logic #Haskell
• Gradual certified programming in Coq. ~ T. Eric & N. Tabareau #Coq
• Graphes et couplages en Coq. ~ C. Dubois et als. #Coq
• HERMIT: An Equational Reasoning Model to Implementation Rewrite System for Haskell. ~ A. Gill #Haskell
• HOCore in Coq. ~ M. Escarrá, P. Maksimović & A. Schmitt #Coq
• Hermite normal form in Isabelle/HOL. ~ J. Divasón & J. Aransay #ITP #Isabelle_HOL #AFP
• Higher-order automated theorem provers. ~ C. Benzmüller #ITP
• Hindley-Milner elaboration in applicative style (Functional pearl). ~ F. Pottier #OCaml
• Homotopy type theory: Unified foundations of mathematics and computation. ~ S. Awodey & R. Harper #HoTT #Math #CompSci
• Homotopy type theory. ~ A. Pelayo & M.A. Warren #HoTT
• Hot code reloading in Cloud Haskell. ~ Pankaj More #Haskell
• How to express convergence for analysis in Coq. ~ C. Lelay #Coq
• Hygame: Teaching Haskell using games. ~ Z. Baharav & D.S. Gladstein #Haskell
• Idris: A functional programming language with dependent types. ~ F. Teegen #Idris
• Imperative insertion sort in Isabelle/HOL. ~ C. Sternagel #AFP #Isabelle_HOL
• Innocuous double rounding of basic arithmetic operations. ~ P. Roux #ITP #Coq #JFR
• Interacting with modal logics in the Coq proof assistant. ~ C. Benzmüller & B. Woltzenlogel Paleo #ITP #Coq
• Intermediate Logic. ~ R. Zach #eBook #Logic
• Introducing functional programmers to interactive theorem proving and program verification. ~ I. Sergey & A. Nanevski #ITP #Coq
• Introduction to computational logic. ~ G. Smolka & C.E. Brown #eBook #Logic #Coq
• Isabelle and security. ~ J.C. Blanchette & A. Popescu #Isabelle_HOL
• Krivine nets: A semantic foundation for distributed execution. ~ O. Fredriksson & D.R. Ghica #Agda
• Lattice-based data structures for deterministic parallel and distributed programming. ~ L. Kuper @lindsey #PdD_Thesis #Haskell
• Layers, resources and property templates in the specification and analysis of two interactive systems. ~ J.C. Campos #ITP #PVS
• Learn Physics by programming in Haskell. ~ S.N. Walck #Haskell
• Learning-based relevance filter for Isabelle/HOL. ~ J.C. Blanchette et als. #Isabelle_HOL
• Lenses in functional programming. ~ A. Steckermeier #Haskell
• Lightweight higher-order rewriting in Haskell. ~ E. Axelsson & A. Vezzosi #Haskell
• LiquidHaskell: Experience with refinement types in the real World. ~ N. Vazou, E.L. Seidel & R. Jhala #Haskell
• LiquidHaskell: Refinement types in the real world. ~ N. Vazou, E.L. Seidel & R. Jhala #Haskell #SMT
• Logic and computation. ~ B. Pientka #eBook #Logic #CompSci
• Logic for problem solving, revisited. ~ Robert Kowalski #eBook #Logic #CompSci #LP
• Machine-checked proofs for realizability checking algorithms. ~ A. Katis, A. Gacek, M.W. Whalen #ITP #Coq
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. ~ #Coq
• Maximally permissive controlled system synthesis for modal logic. ~ A.C. van Hulst, M.A. Reniers & W.J. Fokkink #ITP #Coq
• Mechanized network origin and path authenticity proofs– ~ F. Zhang et als. #Coq
• Mechanized support for the formal especification, verification and deployment of component-based applications. ~ N. Gaspar #Coq
• Mechanized verification of fine-grained concurrent programs. ~ I. Sergey, A. Nanevski & A. Banerjee #ITP #Coq
• Mining the Archive of Formal Proofs. ~ J.C. Blanchette, M. Haslbeck, D. Matichuk & T. Nipkow #Isabelle_HOL #AFP
• Modeling human behaviour with Higher Order Logic: insider threats. ~ J. Boender #Isabelle_HOL
• Modeling set theory in homotopy type theory. ~ Jérémy Ledent #HoTT #Coq
• Modelling algebraic structures and morphisms in ACL2. ~ J. Heras, F.J. Martín & V. Pascual. #ITP #ACL2
• Mutual exclusion by four shared bits with not more than quadratic complexity. ~ W.H. Hesselink #ITP #PVS
• Natural language reasoning using Coq: interaction and automation. ~ S. Chatzikyriakidis #Coq
• New arithmetic algorithms for hereditarily binary natural numbers. ~ P. Tarau #Haskell
• Numerical mathematics on FPGAs using CλaSH. ~ M. Bakker #Haskell #Math
• Object-oriented style overloading for Haskell. ~ M. Shields & S. Peyton Jones #Haskell
• On Euclid’s algorithm and elementary number theory. ~ R. Backhouse & J.F. Ferreira #Algorithms
• On the formalization of signal-flow-graphs in HOL. ~ S.M. Beillahi, U. Siddique & S. Tahar #ITP #HOL_Light
• Optimising embedded domain specific languages (eDSL) using template Haskell. ~ L.J. Buit #Haskell
• Optimising purely functional GPU programs. ~ T.L. McDonell #PhD_Thesis #Haskell
• Parsing parses: A pearl of (dependently typed) programming and proof. ~ J. Gross & A. Chlipala #Coq
• Picat: A Logic-based multi-paradigm language. ~ H. Kjellerstrand #LP #FP #Picat #Prolog
• Pointer program derivation using Coq: Graphs and Schorr-Waite algorithm. ~ J.F. Dufourd #ITP #Coq
• Practical principled FRP (Forget the past, change the future, FRPNow!) ~ A. van der Ploeg & K. Claessen #Haskell
• Principles for verification tools: Separation logic. ~ B. Dongol, V.B.F. Gomes & G. Struth #ITP #Isabelle_HOL
• Priorities without priorities: Representing preemption in psi-calculi. ~ J.A. Pohjola & J. Parrow #Isabelle_HOL
• Program verification by coinduction. ~ B. Moore & G. Rosu #ITP #Coq
• Programming with refinement types: An introduction to LiquidHaskell. ~ R. Jhala et als. #eBook #Haskell
• Programs and proofs (Mechanizing mathematics with dependent types). ~ I. Sergey #eBook #ITP #Coq
• Promoting functions to type families in Haskell. ~ R.A. Eisenberg & J. Stolarek. #Haskell
• Propositional calculus in Coq. ~ F.v. Doorn #Logic #ITP #Coq
• Proving tight bounds on univariate expressions in Coq. ~ É. Martin-Dorel & G. Melquiond #ITP #Coq
• QR decomposition in Isabelle/HOL. ~ J. Divasón & J. Aransay #ITP #Isabelle_HOL #AFP
• QuickChick: A Coq framework for verified property-based testing. ~ Z. Paraskevopoulou & C. Hritcu #Coq
• Real-valued special functions: upper and lower bounds. ~ L.C. Paulson #ITP #AFP #Isabelle_HOL
• Reasoning with the HERMIT (Tool support for equational reasoning on GHC core programs). ~ A. Farmer, N. Sculthorpe & A. Gill #Haskell
• Refinement to certify abstract interpretations, illustrated on linearization for polyhedra. ~ S. Boulmé & A. Maréchal #Coq
• Refinement types For Haskell. ~ N. Vazou et als. #Haskell
• Relative monads formalised. ~ T. Altenkirch, J. Chapman & T. Uustalu #Agda #JFR
• Relativistic programming in Haskell (Using types to enforce a critical section discipline). ~ T. Cooper & J. Walpole #Haskell
• Representing game dialogue as expressions in first-order logic. ~ K. Wheeler #Logic #NLP #Clojure
• Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. ~ A. Solovyev #HOL_Light
• Safe zero-cost coercions for Haskell. ~ J. Breitner et als. #Haskell
• Scrap your boilerplate with class: extensible generic functions. ~ R. Lämmel & Simon Peyton Jones. #Haskell
• Security type systems and deduction. ~ T. Nipkow & A. Popescu #Isabelle_HOL
• Semantics for programming languages with Coq encodings. ~ Y. Bertot #Coq
• Semantics of intuitionistic propositional logic: Heyting algebras and Kripke models. ~ C.E. Brown #Logic #ITP #Coq
• Sets, the axiom of choice, and all that: A tutorial. ~ E.E. Doberkat #Math #Logic #CompSci
• Simple balanced binary search trees. ~ P. Ragde #Haskell
• SmartCheck: Automatic and efficient counterexample reduction and generalization. ~ Lee Pike #Haskell
• Software validation via model animation. ~ A.M. Dutle, C.A. Muñoz, A.J. Narkawicz & R.W. Butler #ITP #PVS
• Some lessons learned on writing predicate logic proofs in Isabelle/Isar. ~ W. Schreiner #ITP #Isabelle_HOL
• Specifying and verifying IP with linear logic. ~ D. Sinclair et als. #ITP #Coq
• Stream fusion in HOL with code generation. ~ A. Lochbihler #ITP #Isabelle_HOL #AFP
• Structures algébriques et programmation. ~ G. Connan. #eBook #Math #Haskell
• Suitability of Haskell for multi-agent systems. ~ T. de Jong #Hakell #MAS
• Systematic verification of the modal logic cube in Isabelle/HOL. ~ C. Benzmüller & M. Claus #ITP #Isabelle_HOL
• Teaching Logic to Information Systems students: Challenges and opportunities. ~ A. Zamansky & E. Farchi #Logic
• Teaching students property-based testing. ~ Clara Benac Earle et als. #FP #Erlang #QuickCheck
• Termination with domain theory. ~ J. Oberhauser #ITP #Coq
• The CAVA automata library. ~ P. Lammich #ITP #Isabelle_HOL
• The Cayley-Hamilton theorem in Isabelle/HOL. ~ S. Adelsberger & S. Hetzl #ITP #Isabelle_HOL #AFP
• The Gilbreath trick: A case study in axiomatisation and proof development in the Coq proof assistant. ~ G. Huet (1991) #ITP #Coq
• The Jordan-Hölder theorem in Isabelle/HOL. ~ J. von Raumer #AFP #Isabelle/HOL
• The Sturm-Tarski theorem in Isabelle/HOL. ~ W. Li #AFP #Isabelle_HOL
• The Unified Policy Framework (UPF). ~ A.D. Brucker, L. Brügger & B. Wolff #ITP #Isabell_HOL
• The arithmetic of even-odd trees. ~ Paul Tarau #Haskell
• The essence of the iterator pattern. ~ J. Gibbons & B.C.d.S. Oliveira #Haskell
• The formalization of discrete Fourier transform in HOL. ~ Z. Shi et als. #ITP #HOL
• The foundational cryptography framework. ~ A. Petcher & G. Morrisett #ITP #Coq
• The maximum segment sum problem: Its origin, and a derivation. ~ Shin-Cheng Mu #Haskell
• The proof is in the plugin. ~ E. Austin & P. Alexander #Haskell
• The proof is in the process. A preamble for a philosophy of computer-assisted mathematics. ~ L. de Mol #ITP
• The selection monad as a CPS translation. ~ J. Hedges #Haskell
• There is no fork: an abstraction for efficient, concurrent, and concise data access. ~ S. Marlow et als. #Haskell
• Thinking with laziness. ~ T. Jelvis #Haskell
• Towards a theory of reach. ~ J. Fowler & G. Hutton #Haskell
• Towards formal fault tree analysis using theorem proving. ~ W. Ahmed & O. Hasan #HOL4 #ITP
• Towards the formalization of fractional calculus in Higher-Order Logic. ~ U. Siddique, O. Hasan & S. Tahar #ITP #HOL_Light
• Tutorial on LiquidHaskell. ~ N. Vazou, E. Seidel, P. Rondon, and R. Jhala #Haskell
• Two axiomatizations of Nelson algebras. ~ A. Grabowski #ITP #Mizar
• Two can keep a secret, if one of them uses Haskell (Functional pearl). ~ A. Russo #Haskell
• Typed faceted values for secure information flow in Haskell. ~ T.H. Austin, K. Knowles & C. Flanagan #Haskell
• Un ordinateur pour vérifier les preuves mathématiques. ~ Assia Mahboubi #Math #CompSci #ITP
• Upon the Haskell support for the web applications development. ~ A. Vasilescu #Haskell
• Validating dominator trees for a fast, verified dominance test. ~ S. Blazy, D. Demange & D. Pichardie #ITP #Coq
• Vector spaces (formalisation of basic linear algebra). ~ H. Lee #ITP #AFP #Isabelle_HOL
• Verification of Faust (Functional Audio Stream) signal processing programs in Coq. ~ E.J. Gallego, O. Hermant & P. Jouvelot #Coq
• Verification of a cryptographic primitive: SHA-256. ~ A.W. Appel #ITP #Coq
• Verification of system FC in Coq. ~ T. Garsyset als. #Coq #Haskell
• Verified correctness and security of OpenSSL HMAC. ~ L. Beringer, A. Petcher, K.Q. Ye @hypotext & A.W. Appel #Coq
• Verified efficient implementation of Gabow’s strongly connected component algorithm. ~ P. Lammich #ITP #Isabelle_HOL
• Verified functional programming in Agda. ~ A. Stump #eBook #FP #Agda
• Verified generation of glue code for ROS-based control systems. ~ W. Meng et als. #Coq
• Verified reachability analysis of continuous systems. ~ F. Immler #ITP #Isabelle_HOL
• Verified validation of program slicing. ~ S. Blazy et als. #ITP #Coq
• Verifying fast and sparse SSA-based optimizations in Coq. ~ D. Demange #ITP #Coq
• Verifying type class laws with equational reasoning. ~ L. Hofmaier #Haskell
• Views of PI: Definition and computation. ~ Y. Bertot & G. Allais #ITP #Coq
• Visualisation of Haskell performance. ~ Peter Moritz Wortmann #PhD_Thesis #Haskell
• Vote counting as mathematical proof. ~ D. Pattinson #ITP #Coq #Haskell
• Worker/wrapper/makes it/faster. ~ J. Hackett & G. Hutton. #Haskell
• Zippers and data type derivatives. ~ S. Roßkopf #Haskell