Name: Going through Software Foundations by Benjamin Pierce et al
Start: 2019-03-08T18:30:00-06:00
End: 2019-03-08T21:30:00-06:00
Location: Barnes and Noble Bookstore/Cafe

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.

Darren Rhea

Austin Types, Theorems, and Programming Languages

Technology

Lisp

Programming Languages

Computer Programming

OCaml Programming

Automated Reasoning

Agda

Type Theory

Category Theory

Formal Methods

Idris

Haskell

Mathematics

Anna Ayzenshtat

Max Loukianov

Going through Software Foundations by Benjamin Pierce et al

Barnes and Noble Bookstore/Cafe

Share

Austin Types, Theorems, and Programming Languages

Going through Software Foundations by Benjamin Pierce et al

Austin Types, Theorems, and Programming Languages

Details

Members are also interested in