Equational Logic for Names and Binders
Ranald Clouston (ANU)
LOGIC AND COMPUTATION SEMINARDATE: 2011-02-01
TIME: 15:30:00 - 16:30:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
Many basic logical systems, particularly in computer science, are described by equations modulated by side conditions asserting that particular names are 'not free for' particular metavariables. These side conditions are non-trivial when names may be 'bound' by some operations, such as lambda-abstraction. Nominal Equational Logic, developed with Andrew Pitts, generalises equational logic to express and reason about these modulated equations.
