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/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**\\
workshop_2.txt · Last modified: 2014/05/30 08:45 by mellies
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