|
|
 |
|
Formal Methods Seminar by Gilles Dowek |
|
Date: March 9, 2007
Time: 10:30am
Location: NIA, Rm 137
Additional Information: Presentation (.pdf)
A Formal Toolbox to Prove Properties of Programming Languages
Gilles Dowek, Ecole Polytechnique
Proving properties of programming languages is often delicate. Writing proofs formally, using a verification system such as PVS of Coq, is often the only safe way to identify the hypotheses that are needed, for a property to be established. We present in this talk a formal toolbox containing various reduction relation constructions and theorems that state that these constructions preserve some properties such as determinism and compositionality. This toolbox has been used to prove properties of NASA's Plan Execution Interchange Language (PLEXIL), buy may also be used to prove properties of other programming languages.
|
|
|
Home