Sept 9, 2011: Seminar History and Initial Planning Meeting
Bob's notes: PDF
Sept 16, 2011: NuPRL Demo
Mark Bickford will demonstrate the Nuprl system in action. He will start by showing how to state and prove simple theorems in logic and number theory and extract efficient programs from the proofs. He will also illustrate some elements of Event Logic in specifying a protocol. If there is time he will show some proofs he created this summer while tracking results of Dexter Kozen and Alexandra Silva as they were developing them. His investigations reveal a need to take a closer look at Brouwer's ideas about continuity as a general property of computable functions.
Sept 23, 2011:
Analyzing Access Control Logics Using Evidence Semantics
It is known that access control logics can be given a clear semantics using realizability. Abadi has written about this as well as several other authors, and there is a mapping of Abadi's particular logic, CDD, into system F. However, in his paper Variations in Access Control Logic from 2008 [PDF from Springer], he does not employ realizability. I will interpret his results using evidence semantics because the proofs can be made simpler, they suggest implementation ideas, and because his results illustrate a principle that Mark and I advance: the natural logic of distributed computing is intuitionistic.
Oct 7, 2011: Image Type: A New Type Constructor.
Mark Bickford presenting Alexie Kopylov's work on Image Type: A New Type Constructor.
Reference: Nogin & Kopylov's 2006 paper Formalizing Type Operations Using the "Image" Type Constructor
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. 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.
Noc 4: Discussion of Simple Consensus Algorithm Continued
Nov 18:A Conversation with Moshe Vardi
Join in a discussion with Professor Vardi on the topic of Logic in Computer Science.
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
This "functional necklace" aims to change how you try to write your next interpreter: by deforesting the object language, to exhibit more static safety in a simpler type system. We show how easy it is to build a family of interpreters for a typed object language (such as the simply typed lambda calculus) in a typed metalanguage (such as Haskell or ML) that preserve types without using dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The interpreters include an evaluator, a compiler, a partial evaluator, and call-by-name and call-by-value CPS transformers.
Our main idea is to encode abstract syntax using cogen functions rather than data constructors. In other words, we represent object terms not in an initial algebra but in an arbitrary algebra. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformation. Our encoding of an object term abstracts over the various ways to interpret it, yet statically assures that the interpreters never get stuck.
Dec 9: A Discussion of the Nuprl Evaluator