Grupo de Lógica Computacional

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