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/30 08:33]
streicher [Lectures]
workshop_2 [2014/05/30 08:45] (current)
mellies
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**\\
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