These are draft papers, not submitted except where noted. Please send me a note if you're interested in something below.
A predicative type system with power types is introduced and studied, based on a reformulated fragment of Cardelli's 1988 system with power types. It allows better logical encodings than LF or LambdaPsub, and has an alternative way of expressing higher order subtyping.
This white paper describes proposals for the Proof General Kit, a continuation of the Proof General project. The Kit introduces a new architecture for Proof General. Instead of a monolithic implementation inside Emacs, Proof General will become a collection of communicating components. The aim is to allow a flexible interoperability between various user interface elements (including Emacs), proof engines, and other proof tools. In the spirit of the present system, we want to achieve this using carefully designed lightweight protocols, which are easily supported by a range of present and future proof engines. The protocols and components will be developed in stages, by successive generalization.
This paper outlines the design of a protocol for interactive electronic proof. The design has been influenced by the generic mechanisms that Proof General uses to communicate with various interactive proof assistants. The new protocol, PGIP, is a rationalization of these mechanisms, proposed as an open standard for future proof assistants to support. Messages in PGIP are small XML documents. PGIP comes with an associated markup language PGML for representing structural aspects of concrete syntax.