Registration
This shows you the differences between two versions of the page.
|
workshop_2 [2014/05/17 10:52] 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) : 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 44: | 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 50: | 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|//Duality of computation and polarities//|| | + | |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|//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 73: | Line 75: | ||
| //Intuitions for cubical methods in nonabelian algebraic topology// | //Intuitions for cubical methods in nonabelian algebraic topology// | ||
| - | > The talk will start from the 1-dimensional Seifert-van-Kampen Theorem for the fundamental group, then groupoid, and so to a use of certain strict multiple groupoids for higher versions. These allow for some precise nonabelian calculations of homotopy types, obtained by a gluing process. Cubical methods are important because of the ease of writing multiple compositions, leading to "algebraic inverses to subdivision", relevant to higher dimensional local-to-global problems. Also the proofs involve some ideas of 2-dimensional formulae and rewriting. The use of *strict* multiple groupoids is essential to obtain homotopy type descriptions as *colimits* and hence precise calculations.// | + | > The talk will start from the 1-dimensional Seifert-van-Kampen Theorem for the fundamental group, then groupoid, and so to a use of certain strict multiple groupoids for higher versions. These allow for some precise nonabelian calculations of homotopy types, obtained by a gluing process. Cubical methods are important because of the ease of writing multiple compositions, leading to "algebraic inverses to subdivision", relevant to higher dimensional local-to-global problems. Also the proofs involve some ideas of 2-dimensional formulae and rewriting. The use of *strict* multiple groupoids is essential to obtain homotopy type descriptions as *colimits* and hence precise calculations. |
| - | Another idea is to use both a "broad" and a "narrow" model of a particular kind of homotopy types, where the broad model is used for conjectures and proofs, while the narrow model is used for calculations and relation to classical methods. The algebraic proof of the equivalence of the two models then gives a powerful tool, for example for transferring monoidal closed structures from a cubical model. | + | > Another idea is to use both a "broad" and a "narrow" model of a particular kind of homotopy types, where the broad model is used for conjectures and proofs, while the narrow model is used for calculations and relation to classical methods. The algebraic proof of the equivalence of the two models then gives a powerful tool, for example for transferring monoidal closed structures from a cubical model. |
| **Cisinski**\\ | **Cisinski**\\ | ||
| Line 83: | 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 102: | Line 107: | ||
| //Sample space-time// | //Sample space-time// | ||
| - | **Munch**\\ | + | **Munch-Maccagnoni**\\ |
| - | //Duality of computation and polarities// | + | //Polarities and classical constructiveness// |
| - | > We shall review the duality of computation (Curien and Herbelin 2000) and its revisitation of the 2010's, by Guillaume Munch, and by Guillaume Munch and myself, under the light of polarities. In particular, we shall present Guillaume Munch's notion of duploid and we will sketch how it can be built upon to provide "direct" categorical models of polarised logics and of languages which allow for a mixture of call-by-name and call-by-value (ongoing work with Marcelo Fiore and Guillaume Munch). We shall also hint at some connections with operads. | + | > 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**\\ | ||