Registration
This shows you the differences between two versions of the page.
|
workshop_2 [2014/05/23 08:42] streicher [Planning] |
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 85: | Line 85: | ||
| > I will discuss different notions of model Martin-Löf's intuitionistic type theory. I will take an intuitionistic perspective follwing Martin-Loef's seminal paper "About models for intuitionistic type theories and the notion of definitional equality" from 1975 and mention both foundational and mathematical aspects. Both game semantic and category theoretic considerations are illuminating and I shall discuss their role. | > I will discuss different notions of model Martin-Löf's intuitionistic type theory. I will take an intuitionistic perspective follwing Martin-Loef's seminal paper "About models for intuitionistic type theories and the notion of definitional equality" from 1975 and mention both foundational and mathematical aspects. Both game semantic and category theoretic considerations are illuminating and I shall discuss their role. | ||
| + | |||
| + | **Hofmann**\\ | ||
| + | //Revisiting the categorical interpretation of type theory// | ||
| **Huber**\\ | **Huber**\\ | ||
| Line 104: | 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**\\ | ||