Lab Lunch calendar

Recent Posts
Recent Comments
 URL on Two views of programming language design
 My Homepage on Leaving the Nest: variables with interleaving scopes
 Dan Ghica on Categorical semantics of digital circuits
 So what is a “pure programming language” anyway?  The Lab Lunch on Types: computation vs. interaction
 Dan Ghica on A short fable of software engineering vs. regular engineering
Archives
Categories
Meta
Blogroll
 Existential Type, Bob Harper’s blog
 Gagalium OCaml and Coq development team
 Mathematics and Computation, Andrej Bauer’s blog
 Semantic Domain, Neel Krishnaswami’s blog
Category Archives: proof assistants
Two kinds of mathematics
Preliminary reading: “The Origins and Motivations of Univalent Foundations” by V. Voevodsky’s [PDF] “Proofs and refutations” by I. Lakatos [link] “On proofs and progress in mathematics” by W. Thurston [link] I find the recent surge in interest in the use of … Continue reading
Posted in armchair philosophy, proof assistants
1 Comment
Searching/fumbling for a proof assistant
I was always very impressed with people who use proof assistants to do their maths. It seems like something from the future, mechanised, unerring, complicated, slightly incomprehensible, and it makes traditional penandpaper (well, LaTeX) maths seem quaint, artisanal, even obsolete. … Continue reading
Posted in proof assistants
4 Comments