Registration

Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

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

workshop_4 [2014/05/10 20:25] mellies [Planning] |
workshop_4 [2014/06/30 11:02] (current) ong [Planning] |
||
---|---|---|---|

Line 29: | Line 29: | ||

^Monday 23 June||| | ^Monday 23 June||| | ||

|9h30-10h30|//Registration and Introduction//|| | |9h30-10h30|//Registration and Introduction//|| | ||

- | |11h00-12h00|Martin Hofmann|//Abstract Interpretation from Buchi Automata//| | + | |11h00-12h00|Martin Hofmann|//[[https://dl.dropboxusercontent.com/u/75950203/hofmann.pdf|Abstract Interpretation from Buchi Automata]]//| |

- | |14h30-15h30|Olivier Serre|//What are collapsible pushdown automata good for?//| | + | |14h30-15h30|Olivier Serre|//[[http://www.liafa.univ-paris-diderot.fr/~serre/IHP/IHP_Serre_Full.pdf|What are collapsible pushdown automata good for?]]//| |

|16h00-17h00|Sylvain Salvati|//Models for model checking higher-order programs//| | |16h00-17h00|Sylvain Salvati|//Models for model checking higher-order programs//| | ||

^Tuesday 24 June||| | ^Tuesday 24 June||| | ||

- | |9h30-10h30|Jens Palsberg|// //| | + | |9h30-10h30|Jens Palsberg|//Efficient Inference of Packed Locality Types//| |

- | |11h00-12h00|Giuseppe Castagna|//Polymorphic Functions with Set-Theoretic Types//| | + | |11h00-12h00|Giuseppe Castagna|//[[http://www.pps.univ-paris-diderot.fr/~gc/slides/polydeuces-slides.pdf|Polymorphic Functions with Set-Theoretic Types]]//| |

- | |14h30-15h30|Ranjit Jhala|//Liquid Types For Haskell//| | + | |14h30-15h30|Ranjit Jhala|//[[http://goto.ucsd.edu/~rjhala/IHP14/lhs/Index.lhs.slides.html|Liquid Types For Haskell]]//| |

- | |16h00-17h00|Jakob Rehof|//Types as Programs: Foundations of Combinatory Logic Synthesis//| | + | |16h00-17h00|Jakob Rehof|//[[https://dl.dropboxusercontent.com/u/75950203/rehof.pdf|Types as Programs: Foundations of Combinatory Logic Synthesis]]//| |

|from 18h|//Cocktail at the Institut Henri Poincaré//|| | |from 18h|//Cocktail at the Institut Henri Poincaré//|| | ||

^Wednesday 25 June||| | ^Wednesday 25 June||| | ||

- | | 9h30-10h30|Andrey Rybalchenko|//Solving (quantified) Horn constraints for program verification and synthesis//| | + | | 9h30-10h30|Andrey Rybalchenko|//[[https://dl.dropboxusercontent.com/u/75950203/rybalchenko.pdf|Solving (quantified) Horn constraints for program verification and synthesis]]//| |

- | |11h00-12h00|Helmut Seidl|//Efficiently intertwining widening and narrowing//| | + | |11h00-12h00|Helmut Seidl|//[[https://dl.dropboxusercontent.com/u/75950203/seidl.pdf|Efficiently intertwining widening and narrowing]]//| |

^Thursday 26 June||| | ^Thursday 26 June||| | ||

- | | 9h30-10h30|Colin Stirling|//Deciding equivalence using type checking//| | + | | 9h30-10h30|Colin Stirling|//[[http://homepages.inf.ed.ac.uk/cps/paris.pdf|Deciding equivalence using type checking]]//| |

- | |11h00-12h00|Kazushige Terui|//On applications of models of linear logic//| | + | |11h00-12h00|Kazushige Terui|//[[https://dl.dropboxusercontent.com/u/75950203/terui.pdf|On applications of models of linear logic]]//| |

|14h30-15h30|Paul-André Melliès|//Linear logic and higher-order model-checking//| | |14h30-15h30|Paul-André Melliès|//Linear logic and higher-order model-checking//| | ||

- | |16h00-17h00|Pierre Clairambault|//Strategies as Higher-Order Recursion Schemes//| | + | |16h00-17h00|Pierre Clairambault|//[[http://perso.ens-lyon.fr/pierre.clairambault/Clairambault-IHP260614.pdf|Strategies as Higher-Order Recursion Schemes]]//| |

^Friday 27 June||| | ^Friday 27 June||| | ||

- | | 9h30-10h30|Rupak Majumdar|//Abstractions in the Continuous World//| | + | | 9h30-10h30|Rupak Majumdar|//[[http://www.mpi-sws.org/~rupak/Talks/IHP2014.ppt|Abstractions in the Continuous World]]//| |

- | |11h00-12h00|Mikolaj Bojanczyk|//Computing with atoms//| | + | |11h00-12h00|Mikolaj Bojanczyk|//[[http://www.mimuw.edu.pl/~bojan/slides/atoms-ihp.swf|Computing with atoms]]//| |

===== Preliminary list of invited speakers ===== | ===== Preliminary list of invited speakers ===== | ||

* Mikolaj Bojanczyk (Warsaw, Poland) | * Mikolaj Bojanczyk (Warsaw, Poland) | ||

Line 91: | Line 91: | ||

**Giuseppe Castagna**\\ | **Giuseppe Castagna**\\ | ||

//Polymorphic Functions with Set-Theoretic Types// | //Polymorphic Functions with Set-Theoretic Types// | ||

- | > We present a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation). In a first part we define and study the explicitly-typed version of the calculus in which type instantiation is driven by explicit instantiation annotations. In particular, we define an explicitly-typed λ-calculus with intersection types and an efficient evaluation model for it. In the second part, we define a local type inference system that allows the programmer to omit explicit instantiation annotations, and a type reconstruction system that allows the programmer to omit explicit type annotations. This work provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data. | + | |

+ | > In set-theoretic types systems, types are interpreted as sets of values, unions, intersections and negations of types as the corresponding set-theoretic operations, and the subtyping relation as set containment. | ||

+ | | ||

+ | > Set-theoretic types are useful to give very precise typing to operations on standard functional data structures and are at the basis of type systems for languages that manipulate XML documents. | ||

+ | | ||

+ | > In this talk we show how to add polymorphism to set-theoretic type systems. More precisely, we present a calculus with higher-order polymorphic functions, recursive types with arrow and product type constructors and set-theoretic type connectives (union, intersection, and negation). First we define and study the explicitly-typed version of the calculus in which type instantiation is driven by explicit instantiation annotations and study an efficient evaluation model for it. In the second part, we define a local type inference system that allows the programmer to omit explicit instantiation annotations, and a type reconstruction system that allows the programmer to omit explicit type annotations. This work provides the theoretical foundations and technical machinery needed to design and implement higher-order polymorphic functional languages for semi-structured data. | ||

**Pierre Clairambault**\\ | **Pierre Clairambault**\\ | ||

Line 135: | Line 140: | ||

> The main purpose of this talk will be to discuss a series of recent connections between linear logic and higher-order model checking. I will start by explaining how a careful inspection of the work by Kobayashi and Ong on higher-model checking reveals that priorities (or colors) behave there in just the same comonadic way as the exponential modality of linear logic. Then, adding to this observation the elegant correspondence established ten years ago by Bucciarelli and Ehrhard between indexed linear logic and the relational semantics of linear logic, I will explain how to construct a semantic and modular account of colors in higher-order model-checking. This is joint work with Charles Grellois. | > The main purpose of this talk will be to discuss a series of recent connections between linear logic and higher-order model checking. I will start by explaining how a careful inspection of the work by Kobayashi and Ong on higher-model checking reveals that priorities (or colors) behave there in just the same comonadic way as the exponential modality of linear logic. Then, adding to this observation the elegant correspondence established ten years ago by Bucciarelli and Ehrhard between indexed linear logic and the relational semantics of linear logic, I will explain how to construct a semantic and modular account of colors in higher-order model-checking. This is joint work with Charles Grellois. | ||

+ | |||

+ | |||

+ | **Jens Palsberg**\\ | ||

+ | //Efficient Inference of Packed Locality Types// | ||

+ | > In a distributed program, local access is much faster than remote access. As a help to programmers, some distributed languages like X10 require all accesses to be local and enable programs to shift the place of computation to gain access to remote data. In response, researchers have presented static analyses and type systems that determine conservatively whether all accesses are local. Those approaches can distinguish between local and remote data, and they can track place correlation between objects. Yet they cannot handle the Multi Place Idiom for safe use of a field that over time holds objects from different places. We present a type system with packed locality types, which are a light-weight form of existential types that enable us to type check the Multi Place Idiom. A well-typed program does only local access and can shift the place of computation. We present an O(n^4) time type inference algorithm that enables programmers to type check annotation-free programs, and we prove that the inference problem is P-complete. Our example language is a small extension of the Abadi-Cardelli object calculus with three constructs for distributed programming. We have implemented our algorithm and run it on a suite of challenge programs. Joint work with Riyaz Haque. | ||

**Jakob Rehof**\\ | **Jakob Rehof**\\ | ||

Line 181: | Line 191: | ||

> | > | ||

> This connection could be perhaps generalized: any REL-like model (eg. coherent semantics) of linear logic leads to an intersection-like type system. While it would be interesting to develop a general theory, we are rather interested in finding applications of such models and type systems. In this talk, we will discuss our ongoing work in this direction. | > This connection could be perhaps generalized: any REL-like model (eg. coherent semantics) of linear logic leads to an intersection-like type system. While it would be interesting to develop a general theory, we are rather interested in finding applications of such models and type systems. In this talk, we will discuss our ongoing work in this direction. | ||

- | |||

===== Organizers ===== | ===== Organizers ===== | ||

* [[igw@labri.fr|Igor Walukiewicz]] | * [[igw@labri.fr|Igor Walukiewicz]] | ||

* [[luke.ong@comlab.ox.ac.uk|Luke Ong]] | * [[luke.ong@comlab.ox.ac.uk|Luke Ong]] |

Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.