Lecture Videos

• the Problem with Halting running time: 50 minutes 3 seconds; transcript
  
  This video is based on several papers. A version of this talk was presented at COMPUTING 2011 Symposium on 75 years of Turing Machine and Lambda-Calculus, Karlsruhe Germany, 2011 October 20-21. Another version was presented at the 50th anniversary of IFIP WG2.1 in Rome on 2012 February 7, and at UofT on my retirement 2012 June 12. Other versions were given at WST Workshop on Termination, Oxford, 2018 July 18 and at Waterloo, McMaster, and at Newcastle 2018 July 20. The Halting Problem is a version of the Liar's Paradox. I examine specifications for dependence on the agent that performs them. I look at the consequences for the Church-Turing Thesis and for the Halting Problem.
  
  
• from Boolean Algebra to Unified Algebra running time: 48 minutes 40 seconds; transcript
  
  This video is based on the paper from Boolean Algebra to Unified Algebra prepared for the 150th anniversary of George Boole's amazing paper that introduced boolean algebra to the world, and published in the Mathematical Intelligencer v.26 n.2 p.3-19, 2004. The mathematical details are in the paper Unified Algebra, published in the International Journal of Mathematical Sciences v.1 n.1 p.20-37, 2007. It was an invited talk at Passau, Alberta, York (UK), Newcastle, Lisbon, St.Mary's University (Halifax), Waterloo, McMaster, and Memorial. I also gave this talk at UofT on my retirement, 2012 June 7. Boolean algebra is simpler than number algebra, with applications in programming, circuit design, law, specifications, mathematical proof, and reasoning in any domain. So why is number algebra taught in primary school and used routinely by scientists, engineers, economists, and the general public, while boolean algebra is not taught until university, and not routinely used by anyone? A large part of the answer may be in the terminology and symbols used, and in the explanations of boolean algebra found in textbooks. This paper points out some of the problems delaying the acceptance and use of boolean algebra, and suggests some solutions.
  
  
• Practical Predicative Programming Primer running time: 35 minutes 12 seconds; transcript
  
  This video is based on the book a Practical Theory of Programming. It (or a close relative) was given at a summer school in Turku, at Verified Software: Theories, Tools, and Experiments Toronto, 2008 October 6-9, and at Integrated Formal Methods iFM 2012 June in Pisa. I also gave this talk at UofT on my retirement, 2012 June 8, and at Waterloo, McMaster, and Memorial. I introduce a method of programming from specifications so that each programming step can be checked by a veriIfier. Logic errors can be reported the way syntax errors are reported now. Program verification is easier than you think. Invariants and variants are not explicitly needed. The kinds of comments that programmers write, when formalized, are sufficient. And the proofs are well within the abilities of existing provers.
  
  
• a Probability Perspective running time: 47 minutes 30 seconds; transcript
  
  This video is based on the paper a Probability Perspective published in Formal Aspects of Computing, v.23 n.4 p.391-419, 2011. It was an invited talk at McMaster, UC Irvine, Queen's, Waterloo, Dalhousie, and Memorial. I also gave this talk at UofT on my retirement, 2012 June 11. It could be called "probability meets programming". It draws together four perspectives that contribute to a new understanding of probability and solving problems involving probability. The first is the Subjective Bayesian perspective that probability is affected by one's knowledge, and that it is updated as one's knowledge changes. The problem of assigning prior probabilities disappears according to the Information Theory perspective, which equates probability with information. The main point of the talk is that the formal perspective (formalize, calculate, unformalize) is beneficial to solving probability problems. And finally, the programmer's perspective provides us with a suitable formalism. To illustrate the benefits of these perspectives, the previously open problem of the two envelopes is completely solved.
  
  
• Concurrency running time: 16 minutes 13 seconds; transcript
  
  This video is based on the paper Concurrency, which was an invited paper at a celebration of the work of Jayadev Misra on the occasion of his retirement, 2016 April 29. It surveys the ways in which concurrency has been described formally.
  
  
• Number Representation running time: 46 minutes 39 seconds; transcript
  
  This video is based on the paper Number Representation. It delves into some little known facts about number representation, using the point, the rep, and the quote.
  
  
• Out with a Howl. Four lectures: 2012 June 7, 2012 June 8, 2012 June 11, and 2012 June 12.
  
  This is a series of lectures that I gave on the occasion of my retirement. But the morons who recorded the lectures just recorded me, not the screen with all the formulas that I'm talking about. That makes them useless. The last one, on June 12, begins with me singing some songs, including "Scooping the Loop Snooper", written by Geoffrey K Pullam.