PhD in Computer Science

Confluence in sequent setting

Confluence in sequent setting

Academic year 2014/2015

Sommario del corso

• Program
• Notes
• Teaching tools

Program

We consider an untyped intuitionistic sequent term calculus which is non-confluent. 
The confluence is regained by imposing restrictions on the reduction rules, 

which eliminate the critical pair. In this way two subcalculi, the call-by-name  and the call-by-value  variant are obtained. 

We prove the confluence of the two proposed subcalculi by adapting Takahashi's parallel reductions technique for proving confluence of lambda calculus. 

This is a refinement of the standard Tait and Martin-Lof's proof of the confluence of beta-eta reduction in the lambda calculus.
 We analyse the granularity of reduction rules and then define a new notion of parallel reductions in this framework.
 We then prove the diamond property, which yields the proof of confluence for type free  call-by-value sequent calculus. 
Finally, we show that the diamond property of the new parallel reduction is also applicable to the call-by-name case. 

Confluence of a sequent lambda calculus is usually proved by embedding it
in a calculus already known to be confluent. 
We have developed a direct proof of       
confluence of two sequent subcalculi.

Class schedule

Note

The seminar wil be hold by

Silvia Ghilezan (University of Novi Sad, Serbia)

• Teaching materials
• Exams and finals
• Go to Moodle
• Visit the forums