Latest News
02-09-04	Article about key FDL concepts published by First Monday.
	In Abstract identifiers, intertextual reference and a computational basis for recordkeeping, Stuart Allen addresses the basic management problem of how to alter texts rather freely without ruining the bases for claims depending upon them; this becomes an issue of accounting for various dependencies between texts.
01-21-04	Howe's HOL Library Acquired
	Doug Howe's HOL library, based upon his Importing Mathematics from HOL into Nuprl, is being incorporated into the FDL and incrementally mounted on the Web.
01-06-04	FDL Presentation at NA-MKM '04
	Lori Lorigo was one of the presenters at the Second North American Workshop on Mathematical Knowledge Management, held January 6, 2004, in Phoenix, Arizona. Her talk, entitled Services of the Formal Digital Library (FDL), described some of the project's recent work on accounting mechanisms and search facilities.
11-26-03	Keynote Talk at MKM '03
	Robert Constable was a keynote speaker at the Mathematical Knowledge Management Symposium, held November 25-29 in Edinburgh, Scotland. His presentation was entitled Steps Toward a World Wide Digital Library of Formal Mathematics.
10-28-03	Improved Formula Layout in HTML
	Readability of large formulas (and program sources) requires suitable line breaking within formulas and nested indentation of subformulas. A utility for doing this without human intervention is necessary because of the large number of automatically generated pages containing large formulas. Such a utility is now in use for the FDL web presentation.
09-08-03	Results Presented at TPHOLs Conference
	Collaborations between Cornell and CalTech on content for the FDL are reported at TPHOLs meeting in Rome. Members of the two groups also meet to discuss new API's for the FDL.
08-13-03	PVS proofs (through Graphs) mounted on Web
	Proofs have been added to our web presentation of part of the standard PVS collection of theories (Prelude through Graphs) which was mounted earlier without the proofs.
07-10-03	Marktoberdorf Lecture Notes Released
	Information-Intensive Proof Technology, Bob Constable's lecture notes for the Marktoberdorf 2003 Summer School, is now available on the project's Publications page.
06-20-03	Presentation at LICS'03
	Eli Barzilay gave a presentation on Methods of Reflection which he wrote with Bob Constable and Stuart Allen at LICS'03 in Ottawa, Ontario, Canada.
06-04-03	FDL Annual Report
	An html version of the FDL Annual Report for 2002-2003 is online as "Project Briefing -- June 2003" above.
05-01-03	Red-Black Tree Algorithms Online
	A first posting of Alexei Kopylov's formal representation of the data structure of Red-Black Trees in MetaPRL is now available on the FDL Algorithms page.
04-30-03	Researcher Lori Lorigo gives talk at UC Berkeley
	A talk entitled "An Interactive Digital Library of Algorithmic Knowledge" Given at UC Berkeley in April, 2003 by Cornell researcher Lori Lorigo is linked on the FDL Talks page.
04-08-03	PVS collection through Graphs mounted on Web
	Part of the standard PVS collection of theories (Prelude through Graphs) has been mounted as HTML with links representing references between PVS entities.
03-11-03	FDL Editor access available via VNC
	VNC (Virtual Network Computing) access to the FDL editor is now available.  A password and server name are returned to you which you can then use with your own copy of VNC. Go to FDL Online to view.
03-11-03	Search and Lookup FDL Content in XML format
	Two queries to the FDL are now available online for demonstration purposes: a name search and a lemma lookup. Go to FDL Online to view.  The data is returned in XML format, a standard, to allow integration with other applications and tools.
02-20-03	FDL Navigator Manual online
	The FDL Navigator Manual describes the operations of the first prototype of the formal digital library. It describes the commands for browsing and manipulating library objects through a command interface, called top loop, as well as a highly visual user interface, called the Navigator.