Registration

Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

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

workshop_2 [2014/05/30 08:31] 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 | ||

- | * P. Dybjer (TH Chalmers Gothenburg) : What is a model of 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 | * 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 | ||

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 110: | Line 110: | ||

//Polarities and classical constructiveness// | //Polarities and classical constructiveness// | ||

- | > I will recall what constructive can mean in the context of classical | + | > 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. |

- | 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 (not not 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 (not not 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**\\ |

Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.