The PRL Seminar for this Friday, October 7 will be Mark Bickford presenting Alexei Kopylov's work on the Image Type titled: Image Type: A New Type Constructor.

The seminar will take place in Upson 5126 from Noon-1PM.

Jim

There will be no PRL Seminar this week. We will resume next Friday, October 7.

JE

PRL Seminar for Friday Sept 23

Analyzing Access Control Logics Using Evidence Semantics

Presented by Robert Constable

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, 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.

This week's seminar will take place in Upson 5126 from Noon-1PM.

PRL Seminar for Friday Sept. 16

NuPRL in Action

A demonstration by Mark Bickford

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.

This week's seminar will take place in Upson 5126 from Noon-1PM.

This Friday's Seminar will feature a demonstration of NuPRL by Mark Bickford. Mark is a senior researcher on the PRL team focusing on proof development.

Details will be posted to the website later this week: http://www.nuprl.org/PRLSeminar/default.php

Jim

The Fall 2011 PRL Seminar begins today. This will be a planning meeting for the upcoming series.

We'll meet in Upson 5126 every Friday from Noon-1PM.

Please join us. Bring a brown bag lunch if you wish.

Updates on the seminar will be posted to http://www.nuprl.org/PRLSeminar/default.php

Jim

PRL Seminar Fall 2011

• Fridays Noon-1:00PM
• Meet in Upson Hall Room 5126
• Planning meeting set for Sept. 9

Coinciding with teaching EventML to students in our Formal Methods course, we have posted EventML for download on the CRASH Software page: http://www.nuprl.org/crash/software.php

There are Linux & PC install versions as well as a user's manual with background on Classic ML written by Kreitz & Rahli.

Jim

We've added a To Do List to the Wiki to capture and prioritize ideas for the PRL Project.

Link: To Do List

Jim

I got my first glimpse of EventML today. In the upcoming course on Formal Methods, Bob & Vincent will be teaching EventML. Today was the test of Vincent's installation for PC. We've got a smooth install ready for Win 7 & XP and will be sending it to the students in a week or so.

More info about EventML is on our CRASH project site.

Jim

The PRL Seminar will be held Fridays this fall (2011). Friday 9/9 will be an initial organizing meeting.

The Seminar will take place from Noon-1:00PM  in Upson Hall room 5126.

Please send questions or suggestions for the Seminar to Jim Entwood.

Jim

Details about the EventML software developed as part of the CRASH project were added to the website today.

The summary is at: http://www.nuprl.org/crash/software.php

Jim

We've added several new article to the Publication pages on the nuprl site http://www.nuprl.org/html/publication.html . I'll be digitizing Bob Constable's publication archive over the next couple months and posting additional papers to the site.

Jim

I spoke with Cornell Computer Science CFS staff about the nuprl site, asking for ideas of how to condense all the material and to include some php programming.

One solution we are following up on is to have our own virtual linux server to run the site off of. I think that will work well for us. Hopefully it will eliminate the file permission problem we've been having on the windows server. We’d also setup a development server where pages could be tested before moving to the live server.

Although the change over process will present some challenges, being able to insert linked files for headers, styles, footers, & dynamic bread crumbs should hopefully save time, and allow global changes to site design in the future.

Work also continues on content updates. Today the System & Lectures pages were updated.

Updated notes on the planned website server change: NuPRL Notes for Server Change.pdf

Jim

Another quiet day and a productive one.

Updates were made today to the following pages:

• System
• People
• Other Groups
• Projects

I'm beginning to play around with a general format for headers that includes the PRL logo and search form. I hope to hear from CFS soon on using scripts to load headers & footers into the pages. The current server settings do not allow php or server scripts from files with html extensions.

Google analytics is setup on each of the updated pages as well as the home page and CRASH pages. The first report should be available early September.

Jim

The CRASH project website is now up and running. We plan to use the site to provide information to our collaborators and government funders.

The site is up at http://www.nuprl.org/crash

I am looking for feedback and ideas for the site as it evolves. Please send comments to je277@cornell.edu.