Project Meetings -- Summer 2003

We held an All-PI meeting in August and again met with Michael Kohlhase to advance our collaboration. Below is the agenda for the PI meeting.

ONR MURI All-PI Meeting

August 15-16, 2003 -- Ithaca, NY

Agenda

Friday all day

  1. Status report

    Cornell

    • FDL principles and concepts (abstract object ids, closed maps, certificates, sentinels)
    • FDL navigator and editor
    • PVS libraries
    • Reflection (LIC and PhD thesis)
    • Search (Lori and Kleinberg)
    • Semantics of interoperability (Moran PhD)
    • Algorithms (various contributions, major MetaPRL contributions on Red/Black trees, data structures, graph algorithms)

    Wyoming

    • Peer-to-peer library access
    • Jechlitschek's July visit to Cornell
    • Basic search supported by FDL API -- keyword and opid
    • Boolean combinations of primitive searches -- optimized locally by id comparisons.
    • Graph algorithms (Dijkstra)
    • Category theory support for formal program transformations (LOPSTR paper)
    • HELM projections of Nuprl proofs

    CalTech

    • Formalizing algebra in CSF, in CTT
    • Small formal compiler in MetaPRL

  2. Goals for coming year
    • Expanding API's to the FDL
    • Ties with QPQ and Yale/CMU effort with PVS
    • Ties with OMDoc (see Kohlhase visit Aug 20)
    • Small FDL implementations

  3. Working lunch
    • Discuss other collections (possibly 50K theorems, this is 500 mathematics books)
    • update on progress in Europe, Coq and Helm, HOL and Isabelle HOL, constructive subset of HOL

  4. Goals continued
    • Connections to National Science Digital Library (NSDL)
    • Role of Logic of Events and formalizations for DARPA project on distributed systems

  5. Technical discussions
    • Issues with FDL API's
    • Foundational matters for FDL

  6. Social event at the lake
    • Everyone survives the swimming and boating and the bonfire

Saturday morning
  1. Wyoming plans -- Coordinating software (Stuart and Jim)
  2. Caltech plans -- Kopylov's work as link (Jason and Bob)
  3. Meeting with Michael Kohlhase on Wednesday August 20, 2003
  4. Further discussion of FDL/OMDoc connections, discussion of Mizar and Mizar/OMDoc connection.
  5. Status of EU Network of Excellence plans, role of Cornell and the Yale/CMU/SRI projects.