Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

workshop_2 [2014/05/17 10:53]
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 polaritiesIn particularwe 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 logicas 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 connectivesI will show that this idea is very natural from the point of view of control operatorsleading 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**\\
workshop_2.1400316801.txt.gz · Last modified: 2014/05/17 10:53 by streicher
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0