Pierre-Marie Pédrot (Paris 7, France), Double-glueing: refining models of linear logic through realizability
Schedule
- Feb. 9, 2012, 16:15 - 17:00
Abstract
The double-glueing technique, designed by Hyland and Schalk, is a generalization of the underlying structure common to most models of linear logic. This process transforms constraintless models to finer ones, thanks to an orthogonality refinement that captures stricter notions of proofs and counter-proofs.
This construction is at work in many models of LL and permits a nice factorization of the latter. In addition, it also sheds a new light upon polarization, relaxing the double-orthogonal closure of LL. This results in a better separation between exponentials and shifts.
Actually, double-glueing seems to be a promising way to integrate dependent types and subtyping into linear logic, through realizability, instead of more direct syntactical approaches.
The double-glueing technique, designed by Hyland and Schalk, is a generalization of the underlying structure common to most models of linear logic. This process transforms constraintless models to finer ones, thanks to an orthogonality refinement that captures stricter notions of proofs and counter-proofs.
This construction is at work in many models of LL and permits a nice factorization of the latter. In addition, it also sheds a new light upon polarization, relaxing the double-orthogonal closure of LL. This results in a better separation between exponentials and shifts.
Actually, double-glueing seems to be a promising way to integrate dependent types and subtyping into linear logic, through realizability, instead of more direct syntactical approaches.