Hacker News
- A Gentle Introduction to Liquid Types https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types/ 104 comments
- “Rewrite It in Rust” Considered Harmful? [pdf] https://goto.ucsd.edu/~rjhala/hotos-ffi.pdf 128 comments
- CSolve: Liquid Types-Based C Program Verifier https://goto.ucsd.edu/csolve/ 4 comments
- Liquid Haskell: Haskell as a Theorem Prover [pdf] http://goto.ucsd.edu/~nvazou/thesis/main.pdf 26 comments
- PeaCoq, a UI for Coq http://goto.ucsd.edu/~vrobert/coq-en-stock/blog/2015/06/03/introducing-peacoq/ 8 comments
- LiquidHaskell: Refinement Types via SMT and Predicate Abstraction http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ 3 comments
- Automating Formal Proofs for Reactive Systems http://goto.ucsd.edu/reflex/ 5 comments
- Pointers Gone Wild http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2014/05/28/pointers-gone-wild.lhs/ 65 comments
- Quark: A secure Web Browser with a Formally Verified Kernel http://goto.ucsd.edu/quark/ 78 comments
Lobsters
- ``Rewrite it in Rust'' Considered Harmful? https://goto.ucsd.edu/~rjhala/hotos-ffi.pdf 9 comments c , pdf , rust , security
- Liquid Types https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types/ 17 comments rust
- “Rewrite it in Rust” Considered Harmful? https://goto.ucsd.edu/~rjhala/hotos-ffi.pdf 42 comments rust
- Don’t Look UB: Exposing Sanitizer-Eliding Compiler Optimizations https://goto.ucsd.edu/~gleissen/papers/dontlookub.pdf 18 comments cpp
- "Liquid Haskell: Haskell as a Theorem Prover", Vazou 2016 thesis http://goto.ucsd.edu/~nvazou/thesis/main.pdf 7 comments haskell
- Refinement Reflection: Haskell as a theorem prover http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2016/09/18/refinement-reflection.lhs/ 5 comments haskell
- Introducing PeaCoq: a web frontend for Coq http://goto.ucsd.edu/~vrobert/coq-en-stock/blog/2015/06/03/introducing-peacoq/ 9 comments coq
- Okasaki's Lazy Queues with LiquidHaskell http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2015/01/28/okasakis-lazy-queue.lhs/ 13 comments haskell
- Pointers Gone Wild http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2014/05/28/pointers-gone-wild.lhs/ 75 comments programming
- Abstract Refinement Types. What with the work being made on using an SMT solver in GHC's type checker, might this be a natural direction for GHC to move in? http://goto.ucsd.edu/~rjhala/liquid/abstract_refinement_types.pdf 7 comments haskell
- LiquidHaskell: Pointers Gone Wild http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2014/05/28/pointers-gone-wild.lhs/ 16 comments haskell
- LiquidHaskell: The Advantage of Measures http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2014/02/11/the-advantage-of-measures.lhs/ 3 comments haskell
- LiquidHaskell: Termination Requires Refinements http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/12/14/gcd.lhs/ 6 comments haskell
- Checking Termination With LiquidHaskell http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/12/09/checking-termination.lhs/ 3 comments haskell
- LiquidHaskell: Getting to the bottom of the lie http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/12/02/getting-to-the-bottom.lhs/ 31 comments haskell
- LiquidHaskell Caught Telling Lies http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/11/23/telling_lies.lhs/ 21 comments haskell
- CSV Tables with LiquidHaskell http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/10/10/csv-tables.lhs/ 7 comments haskell
- Quark : A Web Browser with a Formally Verified Kernel http://goto.ucsd.edu/quark/ 6 comments haskell
- A Web Browser with a Formally Verified Kernel http://goto.ucsd.edu/quark/ 163 comments programming
- Quark : A Web Browser with a Formally Verified Kernel http://goto.ucsd.edu/quark/ 85 comments netsec
- Checking Lists Are In Order With LiquidHaskell http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/07/29/putting-things-in-order.lhs/ 3 comments haskell
- Abstracting over Refinements in LiquidHaskell http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/06/03/abstracting-over-refinements.lhs/ 4 comments haskell
- Bounding Vectors - LiquidHaskell http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/03/04/bounding-vectors.lhs/ 3 comments haskell
- LiquidHaskell: KMeans Clustering http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/02/16/kmeans-clustering-i.lhs/ 5 comments haskell
- LiquidHaskell - Refinements 101 (contd.) http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/27/refinements101-reax.lhs/ 8 comments haskell
- LiquidHaskell: Refinement Types in Haskell via SMT http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refinement-types-101.lhs/ 24 comments haskell