Going through Software Foundations by Benjamin Pierce et al

This is a group for people interested in type theory, proof theory, category theory and their application to programming languages, proof assistants, formal verification, etc. We will be starting off with the dependently-typed language Coq and two courses on it, namely Software Foundations by Benjamin Pierce et al, and Adam Chlipala's Certified Programming with Dependent Types. We are going to try to walk a thin line between the pragmatics of using real software systems and understanding type / proof / category theory.

Hopefully we will get everyone up and running with Coq and do a few proofs.

Afterward, We will be going out afterwards for food and drinks somewhere nearby. Discussion in the broad topic area is welcome: ACL2, Agda, ATS, Automated Theorem Proving, Automath, Boogie, Bove-Capretta, Category Theory, Coq, Constraint Programming, Cubical Type Theory, Curry-Howard-Lambek, Dafny, Decision Procedures, Dependent Types, Elaborator Reflection, Formal Methods, Formal Verification, Gentzen's Natural Deduction, Haskell, Hoare Logic, HOL, Homotopy Type Theory, Idris, Integer Programming, Interactive Theorem Proving, Isabelle, JonPRL, Lambda Calculus, Lean Theorem Prover, Logic of Computable Functions, Logic Programming, Mathematical Components, Mathematical Proof, Mathematical Logic, Metamath, Mizar, ML, Model Checking, Model Theory, NuPrl, OCaml, Picat, Prolog, Proof Extraction, Proof Theory, PVS, Quantifier Elimination, QBF solvers, Racket, RedPRL, SAT solvers, SMT solvers, Tactics, TLA+, Twelf, Type Theory, Unification, Verification, Z3, etc.