Registration
This shows you the differences between two versions of the page.
|
workshop_2 [2014/05/23 08:43] streicher [Abstracts] |
workshop_2 [2014/05/30 08:45] (current) mellies |
||
|---|---|---|---|
| Line 31: | Line 31: | ||
| * R. Brown (Bangor Univ.) : Intuitions for cubical models of homotopy types | * R. Brown (Bangor Univ.) : Intuitions for cubical models of homotopy types | ||
| * D.-C. Cisinski (Univ. Toulouse) : Univalence for elegant models of homotopy types | * D.-C. Cisinski (Univ. Toulouse) : Univalence for elegant models of homotopy types | ||
| - | * G. Munch (Univ. Paris 7) : Duality of computation and polarities | ||
| * P. Dybjer (TH Chalmers Gothenburg) : What is a model of intuitionistic type theory | * P. Dybjer (TH Chalmers Gothenburg) : What is a model of intuitionistic type theory | ||
| - | * M. Hofmann (LMU Munich) : TBA | + | * M. Hofmann (LMU Munich) : Revisiting the categorical interpretation of type theory |
| * S. Huber (TH Chalmers Gothenburg) : A Model of Type Theory in Cubical Sets | * S. Huber (TH Chalmers Gothenburg) : A Model of Type Theory in Cubical Sets | ||
| * A. Joyal (Univ. Montreal) : Categorical homotopical logic | * A. Joyal (Univ. Montreal) : Categorical homotopical logic | ||
| * J. Kock (Univ. Aut. Barcelona) : Univalence in locally cartesian closed infinity-category | * J. Kock (Univ. Aut. Barcelona) : Univalence in locally cartesian closed infinity-category | ||
| * P. Martin-Löf (Univ. Stockholm) : Sample space-time | * P. Martin-Löf (Univ. Stockholm) : Sample space-time | ||
| + | * G. Munch-Maccagnoni (Univ. Paris 7) : Polarities and classical constructiveness | ||
| * E. Palmgren (Univ. Stockholm) : Models of dependent types and dependently typed logic and their formalization in type theory | * E. Palmgren (Univ. Stockholm) : Models of dependent types and dependently typed logic and their formalization in type theory | ||
| * V. Voevodsky (Princeton) : B-systems - a link which connects the syntax of dependent type theories with their semantics | * V. Voevodsky (Princeton) : B-systems - a link which connects the syntax of dependent type theories with their semantics | ||
| Line 45: | Line 45: | ||
| ^Monday 2 June||| | ^Monday 2 June||| | ||
| |10h30-12h00|Per Martin-Löf|//Sample space-time //|| | |10h30-12h00|Per Martin-Löf|//Sample space-time //|| | ||
| - | |14h00-15h30|Peter Dybjer|//What is a model of type theory//| | + | |14h00-15h30|Peter Dybjer|//What is a model of intuitionistic type theory//| |
| |16h00-17h30|Steve Awodey|//Natural Models of Type Theory//| | |16h00-17h30|Steve Awodey|//Natural Models of Type Theory//| | ||
| ^Tuesday 3 June||| | ^Tuesday 3 June||| | ||
| Line 51: | Line 51: | ||
| |14h00-15h30|Erik Palmgren|//Models of dependent types and dependently typed logic and their formalization in type theory//| | |14h00-15h30|Erik Palmgren|//Models of dependent types and dependently typed logic and their formalization in type theory//| | ||
| ^Wednesday 4 June||| | ^Wednesday 4 June||| | ||
| - | |10h30-12h00|Guillaume Munch|//Polarities and classical constructiveness//|| | + | |10h30-12h00|Guillaume Munch-Maccagnoni|//Polarities and classical constructiveness//|| |
| |14h00-15h30|Joachim Kock|//Univalence in locally cartesian closed infinity-category//| | |14h00-15h30|Joachim Kock|//Univalence in locally cartesian closed infinity-category//| | ||
| - | |16h00-17h30|Martin Hofmann|//TBA//| | + | |16h00-17h30|Martin Hofmann|//Revisiting the categorical interpretation of type theory//| |
| ^Thursday 5 June||| | ^Thursday 5 June||| | ||
| |10h30-12h00|Denis-Charles Cisinski|//Univalence for elegant models of homotopy types//|| | |10h30-12h00|Denis-Charles Cisinski|//Univalence for elegant models of homotopy types//|| | ||
| Line 87: | Line 87: | ||
| **Hofmann**\\ | **Hofmann**\\ | ||
| - | //TBA// | + | //Revisiting the categorical interpretation of type theory// |
| **Huber**\\ | **Huber**\\ | ||
| Line 107: | Line 107: | ||
| //Sample space-time// | //Sample space-time// | ||
| - | **Munch**\\ | + | **Munch-Maccagnoni**\\ |
| //Polarities and classical constructiveness// | //Polarities and classical constructiveness// | ||
| - | > | + | > I will recall what constructive can mean in the context of classical logic, as accounted for by double negation translations and control operators in programming. Girard proposed a few years back a classical sequent calculus where negation is strictly involutive (¬¬A = A) by taking formally into account the polarity of connectives. I will show that this idea is very natural from the point of view of control operators, leading us to a natural deduction where negation is involutive (¬¬A ≅ A). One of the main aspect is that we do not consider that composition needs to be associative when the middle map is from positives to negatives. In a second time I will therefore introduce duploids, which characterises this non-associative composition directly, and relate them to adjunctions. |
| **Palmgren**\\ | **Palmgren**\\ | ||