Study of intensional and extensional properties of Open-Call-By-Value
Open-Call-By-Value is a the name of a set of calculi that change Plotkin's Call-By-Value to allow the reduction of redexes that are usually considered stuck. The Fireball Calculus, that belongs to the set, solves the problem by means of explicit substitutions at a distance. Accattoli and Guerrieri proved the operational equivalence of those calculi. However, the equivalence fails when contextual closure is taken in accoun.
The candidate will study the intensional and extensional properties of calculi defined via explicit substitutions at a distance. In particular, he will develop a variant of the Fireball Calculus that implements Open-Call-By-Value preserving all the good properties of the Fireball Calculus w.r.t. complexity of reduction. In addition, the new variant will be contextually bisimilar to the other variants of Open-Call-By-Value.
This job comes from a partnership with Science Magazine and