Theory

Initial discussion of panel agenda by David Naumann — last modified 2006-01-13 09:07

Dave's excerpts from December 2005 email about focus of panel.

Theory roadmap outline — last modified 2006-04-03 16:59

SUPERSEDED BY Working Outline

Theory Challenges by David Naumann — last modified 2006-04-04 09:39

***** SUPERSEDED by [[Outline of Theory Challenges]] *****

Goals of Unifying Theories — last modified 2006-03-29 19:30

Unifying theories is one of the major goals for every branch of science, and it is considered worthy of pursuit as an intellectual achievement for its own sake. A successful unification demonstrates ...

Linking the Verification of Compilable Code to the Application Content of Computer Based Systems by David Naumann — last modified 2006-03-30 07:51

paper by Egon Boerger

Working outline — last modified 2006-07-07 07:08

Introduction

Outline of Theory Challenges — last modified 2006-10-02 05:35

Outline of theory challenges

System Modeling Challenges — last modified 2006-04-02 14:58

Some of the discussion in the Correct by Construction panel is concerned with designing languages to take verification into account. Do we know which features of current languages really need to be ...

Correctness of Multistage Notations by Peter Sestoft — last modified 2006-04-02 15:53

Correctness of Multistage Notations The goal is to provide the theoretical foundation for moving away from the classical static compile-link-run model of language semantics to where meta-...

Imperative Program Logics by David Naumann — last modified 2006-04-24 22:16

Imperative program logics

Draft Manifesto — last modified 2006-04-23 18:05

Draft Manifesto (?) for the VS grand challenge

Type Systems by David Naumann — last modified 2006-04-20 21:31

(By Steve Zdancewic)

JBook Milestone by David Naumann — last modified 2006-04-24 02:28

**Milestone** for compiler verification

Secure Flow Checking by David Naumann — last modified 2006-04-21 21:39

Verified secure flow checker

Compiler Verification by David Naumann — last modified 2006-07-07 15:29

Context

draft slides for Dagstuhl by David Naumann — last modified 2006-07-07 16:05

 

Concurrency by Peter O'Hearn — last modified 2006-10-02 06:55

Reasoning about concurrency has always been extremely difficult, and the need for workable theories is set to rise with the increasing appearance of multi-core processors.

Draft report Feb 2007 - latex by David Naumann — last modified 2007-02-22 09:53

 

Draft report Feb 2007 - pdf by David Naumann — last modified 2007-02-22 09:53