A Proof Assistant Prototype Based on Algebraic Effects and Handlers - Andrej Bauer

Andrej Bauer
University of Ljubljana, Slovenia; Member, School of Mathematics
March 21, 2013
For more videos, visit video.ias.edu

[@danielsmith5626]

9:31 This is my new favorite CompSci quote.

[@todorgenov5372]

Chiming in 4 (or 7) years too late, but isn't the idea of operator precedence (around minutes 25 to 33) trivially explained using S-expressions [1]? If you use LISP then the example of 3 + (4 + 5) becomes (+ 3 (+ 4 5)). Also, any discussions about 'judgmental equality' can be trivially distinguished between the eq? and = operators in LISP [2] (eq? eq? =) is false. (= eq? =) is a type error There is much to be said about LISP's eval() [3] operator/function, which is supposedly the same thing as an inverse function [4] [1] en.wikipedia.org/wiki/S-expression [2] repl.it/repls/RigidDarlingInterfaces [3] en.wikipedia.org/wiki/Eval [4] math.stackexchange.com/questions/2690953/what-is-the-equivalent-of-eval-function-in-math-notations

[@Lingonvinge]

Thanks for uploading!