[TYPES/announce] Postdoc position at Paris Diderot University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] RAPIDO -- Reasoning And Programming with Infinite Data-Objects. (http://www.irif.fr/~saurin/RAPIDO) * postdoc positions in RAPIDO project: We are opening a post-doc position in RAPIDO project, which is aimed at studying logical methods and tools for enhancing reasoning and programming on infinite data. The post-doc would start sometimes during the fall 2018 (start date between october 2018 and january 2019). RAPIDO is an ANR-funded project hosted at Paris Diderot University involving researchers from three french labs: IRIF (Univ Paris Diderot), LIP (ENS Lyon) and LSV (ENS Paris Saclay). It is coordinated by Alexis Saurin (IRIF lab, sau...@irif.fr) and the post-doc position will administratively be hosted by Paris Diderot University. RAPIDO aims at gathering young researchers to investigate the applicability of proof-theoretical methods to reason and program on infinite data objects. The goal of the project is to develop logical systems capturing infinite proofs (proof systems with least and greatest fixed points as well as infinitary proof systems), to design and to study programming languages for manipulating infinite data such as streams both from a syntactical and semantical point of view. Moreover, the ambition of the project is to apply the fundamental results obtained from the proof- theoretical investigations (i) to the development of software tools dedicated to the reasoning about programs computing on infinite data, e.g. stream programs (more generally coinductive programs), and (ii) to the study of properties of automata on infinite words and trees from a proof-theoretical perspective with an eye towards model-checking problems. * Topics and requirements for applicants We are looking for young researchers who can contribute to the research topics of RAPIDO. Candidates should hold a PhD in computer science or a closely related field (or be close to complete their PhD) with skills in formal methods and logic and a strong expertise in at least one of the following topics: * automata theory, coinduction, cyclic and infinitary proofs, denotational semantics, functional programming, games and game semantics, infinitary rewriting, lazy evaluation, linear logic, MSO logic, proof assistants, proof theory, realizability, streams, temporal logics. * We will be particularly interested in applications of candidates having an experience using the Coq proof assistant, but this is not a requirement for applying! * Important dates: Informal enquiries: as soon as possible Application deadlines: july 18th 2018 Starting date: between october 2018 and january 2019. * Application submission guidelines Applications should be sent to Alexis Saurin before July 18th 2018 in an email entitled "RAPIDO postdoc application", providing: - a detailed CV with a publication list, - a research statement of at most two pages plus bibliography, - and one or two recommendation letters. Potential candidates are strongly encouraged to contact the project coordinator (together with other project members) for informal enquiries as soon as the announcement is released, and at least when *starting* preparing their application (for info on topics such as starting dates, connections with project sites, salary...). More informations on the post-doc position available at: https://www.irif.fr/~saurin/RAPIDO/files/post-doc-announcement-2018.txt Best, Alexis -- Alexis Saurin CNRS researcher, IRIF
[TYPES/announce] PARIS 2018 (FLOC workshop): Deadline extended to *April 25*
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] ** NEW ** - deadline extended to *April 25* - please register your submission title by *April 20* (details below) Call for Papers Programming And Reasoning on Infinite Structures PARIS Workshop Affiliated with FSCD@FLOC 2018 Oxford, UK, July 7&8, 2018 Developing formal methods to program and reason about infinite data, whether inductive or coinductive, is challenging and subject to numerous recent research efforts. The understanding of the logical and computational principles underlying these notions is reaching a mature stage as illustrated by the numerous advances that have appeared in the recent years. Various examples of this can be viewed in recent works on co-patterns, infinite proof systems for logics with induction and coinduction, circular proofs, guarded recursive type theory, research effort on integrated coinduction in proof assistants, concrete semantics of coinductive computation, recent developments in infinitary rewriting, or the unveiling of the Curry-Howard correspondence between temporal logics and functional reactive programming, to name a few. The workshop aims at gathering researchers working on these topics as well as colleagues interested in understanding the recent results and open problems of this line of research: - For outsiders, the workshop will offer tutorial sessions and survey-like invited talks. - For specialists of the topic, the workshop will permit to gather people working with syntactical or semantical methods, people focusing on proof systems or programming languages, and foster exchanges and discussions benefiting from their various perspectives. We are seeking for short submissions (~3-4 pages long, easychair style) presenting (i) new completed results (ii) work in progress, or (iii) advertising recently published results. The workshop is affiliated with FSCD 2018, as part of the Federated Logic Conference of 2018 and is funded by French ANR, RAPIDO project. ** Important dates and submission details: Submission registration (NEW): April 20 Submissions (NEW): April 25 Notification: May 15 Final abstract: May 25 Workshop: July 7 and 8 Submission page: http://easychair.org/conferences/?conf=paris18 Submission style: https://easychair.org/publications/for_authors Website: https://www.irif.fr/~saurin/RAPIDO/PARIS-2018/ ** Program Committee: Andreas Abel (Gothenburg University) David Baelde (ENS Paris-Saclay & Inria Paris; co-chair) Amina Doumane(CNRS and ENS Lyon) Martin Lange (University of Kassel) Rasmus Møgelberg (IT University of Copenhagen) Luke Ong (University of Oxford) Andrew Polonsky (Appalachian State University) Colin Riba (ENS Lyon and CNRS) Alexis Saurin(CNRS and Paris Diderot University; co-chair) Alex Simpson (University of Ljubljana) ** Invited speakers: Bahareh Afshari (University of Gothenburg) James Brotherston (University College London) Pierre Hyvernat (Savoie Mont-Blanc University) ** Topics: Suggested, but not exclusive, topics of interest for the workshop are: - Proof systems: proof system for logics with least and greatest fixed points, infinitary and cyclic/circular proof systems - Calculi: infinitary rewriting, infinitary λ-calculi, co-patterns - Type systems: infinitary type systems, guarded recursive type theory - Curry-Howard correspondence to linear temporal logic and functional reactive programming - Semantics: denotational and interactive semantics for infinite data and computations - Tools: extensions of programming languages and proof assistants to better treat infinite data, results on extending programming languages with primitives for manipulating infinite data such as streams in a more structured and convenient way, coinductive proof methods in proof assistants - Proof theory and verification: the workshop will welcome works demonstrating how proof-theoretical investigations can be applied to model-checking problems, e.g. as in recent studies of higher-order recursive schemes or infinitary proofs.
