Hacker News
- Comparing Objective Caml and Standard ML http://adam.chlipala.net/mlcomp/ 47 comments
- Formal Reasoning About Programs (2017) [pdf] http://adam.chlipala.net/frap/frap_book.pdf 23 comments
- A Program Optimization for Automatic Database Result Caching (2017) [pdf] http://adam.chlipala.net/papers/SqlcachePOPL17/SqlcachePOPL17.pdf 3 comments
- FSCQ: A formally verified crash-proof filesystem [pdf] http://adam.chlipala.net/papers/FscqSOSP15/FscqSOSP15.pdf 18 comments
- Coq: Certified Programming with Dependent Types http://adam.chlipala.net/cpdt/ 33 comments
- Comparing OCaml and Standard ML http://adam.chlipala.net/mlcomp/ 68 comments
- Comparing Standard ML and OCaml http://adam.chlipala.net/mlcomp/ 20 comments
- An Awesome Introduction to Program Verification with Coq http://adam.chlipala.net/cpdt/ 2 comments
Lobsters
- Comparing OCaml and Standard ML http://adam.chlipala.net/mlcomp/ 11 comments ml , programming
- Certified Programming with Dependent Types, by Adam Chlipala http://adam.chlipala.net/cpdt/ 13 comments book , math , programming
- Coq is one of the most fun and enjoyable programming languages I ever use. http://adam.chlipala.net/cpdt/ 25 comments math
- Prototyping a Functional Language using Higher-Order Logic Programming http://adam.chlipala.net/papers/MakamICFP18/MakamICFP18.pdf 3 comments programminglanguages
- The reference info was not found in the current environment. http://adam.chlipala.net/cpdt/ 2 comments coq
- A Setter for Length Indexed Lists http://adam.chlipala.net/cpdt/html/DataStruct.html 8 comments coq
- Point-by-point comparison of OCaml and SML http://adam.chlipala.net/mlcomp/ 12 comments ocaml
- Awesome introduction to Coq for proving programs correct. http://adam.chlipala.net/cpdt/ 15 comments haskell
- Comparing Objective Caml and Standard ML http://adam.chlipala.net/mlcomp/ 30 comments programming
- Certified Programming with Dependent Types http://adam.chlipala.net/cpdt/ 14 comments programming
Lambda the Ultimate
- Print release of a textbook on the Coq proof assistant http://adam.chlipala.net/cpdt/ 5 comments LtU Forum
- Syntactic Proofs of Compositional Compiler Correctness http://adam.chlipala.net/tmp/compose.pdf 4 comments Functional , Implementation , Lambda Calculus , Semantics , Type Theory
- A Verified Compiler for an Impure Functional Language http://adam.chlipala.net/papers/ImpurePOPL10/ 4 comments Functional , Implementation , Lambda Calculus , Semantics , Type Theory
- Certified Programming With Dependent Types Goes Beta http://adam.chlipala.net/cpdt/ 6 comments Functional , Lambda Calculus , Logic/Declarative , Misc Books , Semantics , Teaching & Learning , Type Theory
- A Veriï¬ed Compiler for an Impure Functional Language http://adam.chlipala.net/tmp/imp.pdf 8 comments Functional , Implementation , Lambda Calculus , Semantics
- Parametric Higher-Order Abstract Syntax for Mechanized Semantics http://adam.chlipala.net/papers/PhoasICFP08/ 1 comment Functional , Implementation , Type Theory