NameDateSize

..25-Jul-20197

READMEH A D25-Jul-20191.2 KiB

SERE.mlH A D25-Jul-201933.2 KiB

SERE.ml.htmlH A D25-Jul-201961.6 KiB

WeakPSLUnclockedSemanticsScript.smlH A D25-Jul-201939.9 KiB

README

1
2This directory contains an experimentation semantics supplied by Johan
3Martensson and (mostly) translated into HOL by Mike Gordon.
4
5 Johan Martensson, PhD            Office: +46 31 7451913
6 R&D                              Mobile: +46 703749681
7 Safelogic AB                     Fax: +46 31 7451939
8 Arvid Hedvalls Backe 4           johan.martensson@safelogic.se
9 SE-411 33 Gothenburg, SWEDEN
10 PGP key ID A8857A60
11 www.safelogic.se
12
13The file SERE.ml defines the syntax and semantics of regular
14expressions, and proves some properties suggested by Johan. This file
15can be read into HOL with the "use" function.  The file SERE.ml.html
16is a version of SERE.ml with HTML in comments. It can be viewed at:
17http://www.cl.cam.ac.uk/~mjcg/PSL/SERE.ml.html
18
19The contents of this directory are
20
21README ................................ This file
22SERE.ml ............................... Syntax and semantics of SEREs
23SERE.ml.html .......................... Version of SERE.ml with HTML comments
24WeakPSLUnclockedSemanticsScript.sml ... Holmake script for separate compilation
25
26To run Holmake including the path directory, use:
27
28   Holmake -I ../path -I ../1.1/official-semantics
29
30Mike Gordon
31Wed Jun 23, 2004
32