Seminar

Recent Seminars

• April 20 - Adding Shared Memory to the General Process Model
  Presented by: Jason Wu
• April 13 - Impredicative vs Predicative Type Theory
  We will discuss impredicative vs predicative type theory. Bob will give an introduction and Mark will describe some new work he just finished and Rich Eaton is implementing to make it easier to manage the restrictions imposed by predicative theories like the computational type theory (CTT) of Nuprl.
• March 9- Robert Constable leads a discussion: Reviewing Nuprl
• Feb 24 - Stronger Role for Recursive Types Needed for Logic of Events
• Feb. 10 - A Discussion in Consensus
  Jason Wu guides us through One Half Consensus. We will demonstrate how it works and explore the different ways we can express this protocol in Event ML.
• Feb. 3 - Recursion and Co-induction in specifying protocols
  We will look closely at an idea from Robbert VanRenesse for adding recursion/co-induction, as a combinator for event classes. We will explore the concept in general and use it to provide an alternative specification of Simple Consensus. We might also discuss the concept of how to obfuscate protocols using synthesis.
  Distributed Recursion slides by Michel Raynal
• Dec 9 - A Discussion of the Nuprl Evaluator
• Dec 2 - Finally tagless, partially evaluated:
  Tagless staged interpreters for simpler typed languages
  Chung-chieh Shan (joint work with Jacques Carette and Oleg Kiselyov)
  Slides available: PDF
• Nov 18:A Conversation with Moshe Vardi
  Join in a discussion with Professor Vardi on the topic of Logic in Computer Science.
• Noc 4: Discussion of Simple Consensus Algorithm Continued
• Oct. 28: Simple Consensus Algorithm
  Bob, Mark and Vincent will illustrate how Event ML and Nuprl cooperate to produce correct-by-construction code for the Simple Consensus Algorithm. This example illustrates many features of Event Logic and of the practical use of Mark's notion of programmable event classes. We will also illustrate how we can introduce diversity into the code at a high level and multiply it as we compile the protocol to production languages.
• Oct 21: A discussion with the PRL team.
  A research meeting concerned with how to post proof material for simple consensus to the Library. We examined formal material as written in Nuprl proofs and in EventML and consider the best ways of organizing this material in the library. Rich displayed the material interactively to help focus the discussion.
• Oct 7: Mark Bickford presenting Alexie Kopylov's work on Image Type: A New Type Constructor. more info »
• Sept 23: Analyzing Access Control Logics Using Evidence Semantics
  Presented by Robert Constable
  more info »
• Sept: 16: NuPRL System in Action by Mark Bickford
  more info »
• Sept 9: Overview of PRL & Seminar History
  Bob's Notes