a small informal symposium on constructivity and computability is arranged
at the Department of Mathematics of Uppsala university on June 9-10. See
below. In case you wish to attend please send me an email. There are few
slots available in the programme for shorter (20 min) or longer (40-50
min) presentations. If you wish give a contributed talk, kindly submit a
short abstract before May 16.
Yours sincerely
Erik Palmgren
(organiser)
------
Symposium on constructivity and computability
in topology, analysis and logic
Uppsala, 9-10 June 2011
Invited speakers include
Josef Berger (Munich)
Thierry Coquand (Chalmers)
Matthew Hendtlass (Leeds)
Hajime Ishihara (JAIST)
Sara Negri (Helsinki)
Dag Normann (Oslo)
Dirk Pattinson (Imperial College)
Jan von Plato (Helsinki)
Peter Schuster (Leeds)
Warwick Tucker (Uppsala)
Venue: ᅵngstrᅵm Laboratory, Lecture Hall 4007, Uppsala.
Accomodation:
-------------
Several speakers are staying at Hotel Uppsala:
http://www.profilhotels.se/hoteluppsala/
Another recommendable hotel is
http://www.akademihotellet.se/
A number of Uppsala hotels can also be found here
It is advisable to book a hotel well in advance.
Dear Colleagues,
a small informal symposium on constructivity and computability is arranged at the Department of Mathematics of Uppsala university on June 9-10. See below. In case you wish to attend please send me an email. There are few slots available in the programme for shorter (20 min) or longer (40-50 min) presentations. If you wish give a contributed talk, kindly submit a short abstract before May 16.
Yours sincerely
Erik Palmgren
(organiser)
------
Symposium on constructivity and computability
in topology, analysis and logic
Uppsala, 9-10 June 2011
Invited speakers include
Josef Berger (Munich)
Thierry Coquand (Chalmers)
Matthew Hendtlass (Leeds)
Hajime Ishihara (JAIST)
Sara Negri (Helsinki)
Dag Normann (Oslo) Dirk Pattinson (Imperial College)
Jan von Plato (Helsinki)
Peter Schuster (Leeds)
Warwick Tucker (Uppsala)
Venue: Ångström Laboratory, Lecture Hall 4007, Uppsala.
Thorsten
On 13 May 2011, at 15:56, Thorsten Altenkirch wrote:
> Hi Erik,
>
> since I am in the area anyway (as you know), I'd like to come to your workshop.
>
> I could give a short talk about the partiality monad, see below.
>
> Cheers,
> Thorsten
>
>
> Thorsten Altenkirch
> University of Nottingham
>
> The Partiality Monad
>
> We introduce the partiality monad which is definable in Type Theory
> with quotient types (corresponding to a pretopos). The partiality
> monad can be used to model partial computations within total type
> theory. We can define a fixpoint combinator but this depends on the
> requirement that the input functional is continous, which is true for
> all definable functions. Can we work in a type theory where this is
> provable?
>
>
>
>
>
> On 6 May 2011, at 19:01, Erik Palmgren wrote:
>
>>
>> Dear Colleagues,
>>
>> a small informal symposium on constructivity and computability is arranged at the Department of Mathematics of Uppsala university on June 9-10. See below. In case you wish to attend please send me an email. There are few slots available in the programme for shorter (20 min) or longer (40-50 min) presentations. If you wish give a contributed talk, kindly submit a short abstract before May 16.
>>
>> Yours sincerely
>>
>> Erik Palmgren
>>
>> (organiser)
>>
>> ------
>>
>> Symposium on constructivity and computability
>>
>> in topology, analysis and logic
>>
>> Uppsala, 9-10 June 2011
>>
>>
>> Invited speakers include
>>
>> Josef Berger (Munich)
>> Thierry Coquand (Chalmers)
>> Matthew Hendtlass (Leeds)
>> Hajime Ishihara (JAIST)
>> Sara Negri (Helsinki)
>> Dag Normann (Oslo) Dirk Pattinson (Imperial College)
>> Jan von Plato (Helsinki)
>> Peter Schuster (Leeds)
>> Warwick Tucker (Uppsala)
>>
>>
>> Venue: ngstrm Laboratory, Lecture Hall 4007, Uppsala.
since I am in the area anyway (as you know), I'd like to come to your workshop.
I could give a short talk about the partiality monad, see below.
Cheers,
Thorsten
Thorsten Altenkirch
University of Nottingham
The Partiality Monad
We introduce the partiality monad which is definable in Type Theory
with quotient types (corresponding to a pretopos). The partiality
monad can be used to model partial computations within total type
theory. We can define a fixpoint combinator but this depends on the
requirement that the input functional is continous, which is true for
all definable functions. Can we work in a type theory where this is
provable?
On 6 May 2011, at 19:01, Erik Palmgren wrote:
>
> Dear Colleagues,
>
> a small informal symposium on constructivity and computability is arranged at the Department of Mathematics of Uppsala university on June 9-10. See below. In case you wish to attend please send me an email. There are few slots available in the programme for shorter (20 min) or longer (40-50 min) presentations. If you wish give a contributed talk, kindly submit a short abstract before May 16.
>
> Yours sincerely
>
> Erik Palmgren
>
> (organiser)
>
> ------
>
> Symposium on constructivity and computability
>
> in topology, analysis and logic
>
> Uppsala, 9-10 June 2011
>
>
> Invited speakers include
>
> Josef Berger (Munich)
> Thierry Coquand (Chalmers)
> Matthew Hendtlass (Leeds)
> Hajime Ishihara (JAIST)
> Sara Negri (Helsinki)
> Dag Normann (Oslo) Dirk Pattinson (Imperial College)
> Jan von Plato (Helsinki)
> Peter Schuster (Leeds)
> Warwick Tucker (Uppsala)
>
>
> Venue: ngstrm Laboratory, Lecture Hall 4007, Uppsala.
ist aber schoen zu wissen, dass Du auch dort sein wirst
Thomas