Changeset 3375

Timestamp:
Jul 1, 2013, 5:53:11 PM (4 years ago)
Author:
sacerdot
Message:

Imp language and its labelled-SOS.

  • The language has function calls restricted to the following shape

x := f(E):l

where l is a post-label to be emitted _after_ f returns

  • All function declarations are of the form

nat f(nat None)

The anonimous variable None is the only one to be local.

  • All named variables are global
File:
1 added

Note: See TracChangeset for help on using the changeset viewer.