Seminar: 2000-01

Chronological Index:
2000-01

Spring '01 Semester

I will finish presenting the modular approach to formalization of the quotient types. I will show how the modular theory I presented in the last two seminars can be used to formalize the notion of collection types. If I have time, I will present the rule that states that a type is uniquely determined by its equivalence relation. I will also show how this new rule can be used to establish Z2 intersect Z3 = Z6 and I will also explain why this equality can not be proven in a theory without the new rule.

April 16 - Alexey Nogin

I will continue presenting my modular approach to quotient and other types in type theory.

April 9 - Alexey Nogin

I will present a new modular approach to formalizing complex types in type theory, in particular - the quotient type. I will show how the new building blocks that I create for the quotient type can be successfully reused for other purposes, in particular - to formalize Mark's collection types.

April 2 - Alexey Kopylov

Alexey will talk about results that he and Alexey Nogin submitted to CSL. One of the topics is a new logic of evidence that is based on the squash operator. In last Monday's lecture I gave a preview of these results by defining the new propositional operator, [A], squash A. Alexey can define a version of Markov's principle with this primitive. This work is part of a general investigation of new propositional logics based on types that Alexey Kopylov and I are discussing and for which more results will be forthcoming this semester.

March 26 - Prof. Robert Constable

We will continue to discuss the NSF ITR proposal, taking input from the seminar.

March 19 - SPRING BREAK - No Seminar

March 12 - Prof. Robert Constable

We will talk about the work we plan to do for NSF and how we will coordinate that with other funded efforts. Christoph and I will share the talk and look at the three sections of the proposal.

March 5 - Amanda Holland-Minkley

I'll be talking about my work on validating a methodology for natural language generation of proofs and my preliminary observations on the connections between Nuprl's formal language and the intermediate language for generation that we use.

February 19 - Alexey Nogin

I will present an overview of several approaches for internalizing proofs and provability in Nuprl type theory with and without Term type and Eli's up/down operator.

February 12 - Eli Barzilay

We will discuss a recent mini-project that I have been working on with Bob and Stuart - "Reflection in First-Order Logic" - an attempted 1st-order language description that can accommodate reflection.

February 5 - Ralph Benzinger

"Automated Higher-Order Complexity Analysis." My non-technical presentation will highlight how we can

and will include a live demonstration of my ACA System vs. The Pigeon Holes.

January 29 - Prof. Robert Constable

"How Nuprl Reasons." Bob will deliver part of his upcoming Yale Colloquium lecture about how Nuprl and MetaPrl reason. He is hoping for feedback. One new topic concerns new (to outsiders) propositional operators derived from type theory.