[TYPES/announce] MFPS 2016 conference
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] MFPS 2016 The 32nd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXII) will take place on the campus of the Carnegie Mellon University, Pittsburgh, USA, between 23 and 26 May 2016. MFPS conferences are dedicated to the areas of mathematics, logic, and computer science that are related to models of computation in general, and to semantics of programming languages in particular. This is a forum where researchers in mathematics and computer science can meet and exchange ideas. The participation of researchers in neighbouring areas is strongly encouraged. Topics include, but are not limited to, the following: bio-computation; concurrent qualitative and quantitative distributed systems; process calculi; probabilistic systems; constructive mathematics; domain theory and categorical models; formal languages; formal methods; game semantics; lambda calculus; programming-language theory; quantum computation; security; topological models; logic; type systems; type theory. We also welcome contributions that address applications of semantics to novel areas such as complex systems, markets, and networks, for example. Conference home page: mfps-2016.au.dk ## INVITED SPEAKERS * Peter Selinger, Dalhousie * Brigitte Pientka, McGill * Steve Brookes, CMU * Nathalie Bertrand, Inria ## TUTORIAL SPEAKERS AND SPECIAL SESSIONS * Peter O'Hearn - Concurrency, special session in honour of Steve Brookes' 60th Birthday * Andrew Appel, Princeton - Verification * Stephen Chong, Harvard - Security * Dan Roy, Toronto - Probabilistic Programming ## SUBMISSION ### Important dates: * Submission Deadline: March 3 * Notification: April 8 * Proceedings: April 18 * Conference: May 23-26 ### Submitting Submissions should be prepared using the [ENTCS Macros](http://www.entcs.org/), in the form of a PDF file not exceeding 15 pages. Submissions are open on [EasyChair](https://easychair.org/conferences/?conf=mfps2016). ### Proceedings A preliminary version will be distributed at the meeting. Final proceedings will appear in ENTCS after the meeting. ## PROGRAM COMMITTEE: Achim Jung, Birmingham, UK Andre Scedrov, UPenn, USA Andrej Bauer, Ljubljana, Slovenia Andrzej Murawski, Warwick, UK, Bart Jacobs, Radboud U, Netherlands Bob Coecke, Oxford, UK Cameron Freer, Cambridge MA, USA Catherine Meadows, NRL , USA Catuscia Palamidessi, INRIA, France Christine Tasson, PPS Paris, France Claudio Russo, MSR Cambridge, UK Dusko Pavlovic, Hawaii, US Helle Hvid Hansen, TU Delft, Netherlands Hugo Herbelin, Paris, France Jean Krivine, Paris, France, Joel Ouaknine, Oxford, UK Lars Birkedal (Chair), Aarhus, Denmark Michael Mislove, Tulane, USA Neel Krishnaswami, Birmingham, UK Paul Blain Levy, Birmingham, UK, Peter Dybjer, Chalmers, Sweden Prakash Panangaden, Montreal, Canada Stefan Milius, Erlangen, Germany Steve Brookes, CMU, USA Steve Zdancewic, UPenn, USA ## LOCAL ORGANISERS: * Steve Brookes -- Lars Birkedal Professor, Head of Department of Computer Science Aarhus University Head of Logic and Semantics Group www.cs.au.dk/~birke birke...@cs.au.dk
[TYPES/announce] PhD positions, application deadline May 1, 2016
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear All, We have openings for PhD students, with application deadline on May 1, 2015. The positions are fully funded and come with a generous scholarship. Please help circulate this call to potential applicants. We are looking for candidates interested in (1) Modular reasoning about concurrent higher-order imperative programs (see http://users-cs.au.dk/birke/modures/). Contact: Lars Birkedal, birke...@cs.au.dk (2) Guarded homotopy theory, a new project aimed at developing type theories combining ideas from guarded type theory and homotopy type theory. Contacts: Lars Birkedal, birke...@cs.au.dk and Bas Spitters, spitt...@cs.au.dk. (3) Language-based Security, in particular mitigating timing attacks. Contact: Aslan Askarov, as...@cs.au.dk. Please see http://talent.au.dk/phd/scienceandtechnology/opencalls/ for how to apply. Best wishes, Lars Birkedal — Lars Birkedal Head of Department of Computer Science, Professor Head of Logic and Semantics Group Department of Computer Science Aarhus University www.cs.au.dk/~birke birke...@cs.au.dk
[TYPES/announce] Assistant and associate professor openings at Aarhus University, Denmark
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear All, Several positions as tenure-track assistant professor or associate professor are available at the Department of Computer Science, Aarhus University (www.cs.au.dk<http://www.cs.au.dk>) starting summer, 2017. The department has research groups within "Algorithms and Data Structures", "Data-Intensive Systems", "Cryptography and Security", "Mathematical Computer Science", "Logic and Semantics", "Ubiquitous Computing and Interaction", "Computer-Mediated Activity", "Use, Design and Innovation", and "Programming Languages". Moreover, we wish to build competencies within Machine Learning and Systems Security. Applicants within the areas of "Data-Intensive systems", "Algorithms and Data Structures", "Machine Learning", and "Systems Security" are of special interest, but applicants within other research areas are also very welcome. The application deadline is January 15th, 2017. Additional details and instructions on how to apply are found at: http://scitech.au.dk/en/about-science-and-technology/vacant-positions/scientific-positions/?tx_peoplexs_pi1%5Bid%5D=862617&tx_peoplexs_pi1%5BportalId%5D=5283&tx_peoplexs_pi1%5Baction%5D=show&tx_peoplexs_pi1%5Bcontroller%5D=Vacancy&cHash=52c836baa95211618f57dfe80bc0046a Best wishes, Lars Birkedal — Lars Birkedal Head of Department of Computer Science, Professor Head of Logic and Semantics Group Department of Computer Science Aarhus University www.cs.au.dk/~birke<http://www.cs.au.dk/~birke> birke...@cs.au.dk
[TYPES/announce] Assistant and Associate Professor positions at Aarhus University, Denmark
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear All, A number of positions as tenure-track assistant professor or associate professor are available at the Department of Computer Science, Aarhus University (www.cs.au.dk<http://www.cs.au.dk/>). Applicants within all areas of computer science are welcome and we would be happy to see applications from readers of the types list! The department has a staff of approximately 125 people including 24 full and associate professors, 2 assistant professors, 25 postdocs and 50 PhD students. The number of students is approximately 1,000. The department is expected to expand significantly over the next 5-6 years, as part of Aarhus University’s strategic effort to increase the number of students graduating in computer science and IT. Deadline: January 5, 2018 (strict) Link to official call text: http://scitech.au.dk/om-science-and-technology/stillinger/videnskabelige-stillinger/?tx_peoplexs_pi1%5Bid%5D=934877&tx_peoplexs_pi1%5BportalId%5D=5285&tx_peoplexs_pi1%5Baction%5D=show&tx_peoplexs_pi1%5Bcontroller%5D=Vacancy&cHash=4df9e0c7f01222f969518a96fc9dda68<http://scitech.au.dk/om-science-and-technology/stillinger/videnskabelige-stillinger/?tx_peoplexs_pi1[id]=934877&tx_peoplexs_pi1[portalId]=5285&tx_peoplexs_pi1[action]=show&tx_peoplexs_pi1[controller]=Vacancy&cHash=4df9e0c7f01222f969518a96fc9dda68> Please circulate to potential applicants. Thanks, Lars Birkedal — Lars Birkedal Professor Dept. of Computer Science Aarhus University Aabogade 34 8200 Aarhus N Denmark birke...@cs.au.dk<mailto:birke...@cs.au.dk> www.cs.au.dk/~birke<http://www.cs.au.dk/~birke>
[TYPES/announce] Full Professor Position in Aarhus, Denmark
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear All, The Department of Computer Science at Aarhus University, Denmark, has announced a call for a full professor position in computer science. We are looking for candidates in all areas and would welcome applicants from the types list. Application deadline is May 3, 2018. See http://www.au.dk/en/about/vacant-positions/scientificpositions/stillinger/Vacancy/show/965870/5283/ for the official call text. You are welcome to contact me at birke...@cs.au.dk<mailto:birke...@cs.au.dk> if you have any questions about the position. Best wishes, Lars -- Lars Birkedal Professor www.cs.au.dk/~birke<http://www.cs.au.dk/~birke> birke...@cs.au.dk<mailto:birke...@cs.au.dk>
Re: [TYPES/announce] Full Professor Position in Aarhus, Denmark
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Apologies, the link below was broken. The correct link is http://www.au.dk/en/about/vacant-positions/scientific-positions/stillinger/Vacancy/show/965870/5283/ Best, Lars. On 22 Mar 2018, at 15:24, Lars Birkedal mailto:birke...@cs.au.dk>> wrote: Dear All, The Department of Computer Science at Aarhus University, Denmark, has announced a call for a full professor position in computer science. We are looking for candidates in all areas and would welcome applicants from the types list. Application deadline is May 3, 2018. See http://www.au.dk/en/about/vacant-positions/scientificpositions/stillinger/Vacancy/show/965870/5283/ for the official call text. You are welcome to contact me at birke...@cs.au.dk<mailto:birke...@cs.au.dk> if you have any questions about the position. Best wishes, Lars -- Lars Birkedal Professor www.cs.au.dk/~birke<http://www.cs.au.dk/~birke> birke...@cs.au.dk<mailto:birke...@cs.au.dk> — Lars Birkedal Professor Dept. of Computer Science Aarhus University Aabogade 34 8200 Aarhus N Denmark birke...@cs.au.dk<mailto:birke...@cs.au.dk> www.cs.au.dk/~birke<http://www.cs.au.dk/~birke>
[TYPES/announce] Lecture Notes on Iris: Higher-Order Concurrent Separation Logic.
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear All, We would like to announce the availability of our Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. http://iris-project.org/tutorial-pdfs/iris-lecture-notes.pdf The lecture notes are intended to serve as an introduction to Iris, a higher-order concurrent separation logic framework implemented and verified in the Coq proof assistant. The Preface describing design choices for the lecture notes is included below, as is the table of contents. The notes start from scratch, but includes advanced material on modular specifications for concurrent modules and even a teaser on logical relations in Iris. Slides for a course taught using the lecture notes are available at http://iris-project.org/tutorial-material.html For more information on Iris, including research papers and Coq implementation, please see http://iris-project.org/ Enjoy! Lars Birkedal and Aleš Bizjak birke...@cs.au.dk abiz...@cs.au.dk -- PREFACE Iris has been developed over several years in joint research involving the Logic and Semantics group at Aarhus University, led by Lars Birkedal, and the Foundations of Programming Group at Max Planck Institute for Software Systems, led by Derek Dreyer. Lately, the development has involved several other international research groups, in particular the group of Robbert Krebbers at TU Delft. The main research papers describing the Iris program logic framework are three conference papers [8, 6, 9] and a longer journal paper with more details on the semantics and the latest developments of the logic [7]. These papers, and several other Iris related research papers, can all be found on the Iris Project web site: iris-project.org At this web site one can also get access to the Coq implementation of Iris. Design Choices It is not obvious how one should introduce a sophisticated logical framework such as Iris, especially since Iris is a framework in more than one sense: Iris can be instantiated to reason about programs written in different programming languages and, moreover, Iris has a base logic, which can be used to define different kinds of program logics and relational models. We now describe some of the design choices we have made for these lecture notes. These lecture notes are aimed at students with no prior knowledge of program logics. Hence we start from scratch and we focus on a particular instantiation of Iris to reason about a core concurrent higher-order imperative programming language, λref,conc. (As Martin Hyland once put it [4]: “One good example is worth a host of generalities”.) We start with high-level concepts, such as Hoare triples and proof rules for those, and then, gradually, as we introduce more concepts, we show, e.g., how proof rules that were postulated at first can be derived from simpler concepts. Moreover, new logical concepts are introduced with concrete, but often artificial, verification examples. The lecture notes also include larger case studies which show the logic can be used for verification of realistic programs. A word of caution to the reader. The beginning of the lecture notes, until about Section 4, is rather formal and abstract. Do not be disheartened by it. This part is needed in order to fix notation, and explain the basic structure of reasoning used in concrete examples of program verification later on. Since the Iris logic involves several new logical modalities and connectives, we present example proofs of programs in a fairly detailed style (instead of the often-used proof outlines). We hope this will help readers learn how the novel aspects of the logic work. We have included numerous exercises of varying degree of difficulty. Some exercises introduce reasoning principles used later in the notes. Thus the exercises are an integral part of the lecture notes, and should not be skipped. When we introduce the logic, we only use intuitive semantics to explain why proof rules are sound. For the time being we refer the reader to a research paper [7] for an extensive description of the model of Iris. There are several reasons for this choice: the formal semantics is non-trivial (e.g., it involves solutions to recursive domain equations); the semantics is really defined for the base logic, which is only introduced later in the notes; and, finally, our experience from teaching a course based on the these lecture notes is that students can learn to use the logic without being exposed to the formal semantics of the logic. Since Iris comes with a Coq implementation, it would perhaps be tempting to teach Iris using the Coq implementation from the beginning. However, we have decided against doing so. The reason is that our students do not have enough experience with Coq to make such an approach viable and, moreover, we believe that, for most
[TYPES/announce] Full Professor Position at Aarhus University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear Types readers, A position as Full Professor is available at the Department of Computer Science, Aarhus University (www.cs.au.dk<http://www.cs.au.dk/>). The Department of Computer Science (www.cs.au.dk<http://www.cs.au.dk>) at Aarhus University is looking for an excellent and visionary Full Professor to push the frontiers of Computer Science research. Aarhus University - an international top-100 University - has made an ambitious strategic investment in a 5-year recruitment plan to radically expand the Department of Computer Science.Therefore, we seek researchers driven by excellence in research and visions for the future digitization agenda, to, join the department and collaborate with our world-class researchers. The position is open from September 1st 2019. See https://international.au.dk/about/profile/vacant-positions/job/full-professorship-in-computer-science-aarhus-university/ for the official call text. Application Deadline: Monday June 3, 2019. Best wishes, Lars — Lars Birkedal Professor, Head of Logic and Semantics Group Department of Computer Science Aarhus University www.cs.au.dk/~birke<http://www.cs.au.dk/~birke> birke...@cs.au.dk
[TYPES/announce] Postdoc and PhD positions in logic and semantics for program verification at Aarhus, Denmark
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Supported by a generous Villum Investigator Grant from VILLUM FONDEN we will start a new Center for Basic Research in Program Verification (CPV) in September 2019 at Aarhus University, Denmark. We are looking for several postdocs and PhD students to work in the Center for Basic Research in Program Verification. Research topics include: extensions of higher-order concurrent separation logics (such as our Iris logic, see iris-project.org), e.g., to reason about distributed systems; probabilistic program logics; logical relations for relational reasoning about safety and security properties; formal modeling of low-level capability machines and secure compilation; guarded cubical type theory; and Coq formalizations. Postdoc positions are for two years initially (can be extended upon mutual agreement). Interested postdoc and PhD candidates are welcome to contact Lars Birkedal . For more information about our previous work, see https://cs.au.dk/~birke/ Postdoc application deadline is July 1, 2019. See https://international.au.dk/about/profile/vacant-positions/job/center-for-basic-research-in-program-verification-cpv-is-looking-for-post-docs/ for the official announcement. PhD applications should be submitted via the Graduate School of Science and Technology application website: http://phd.scitech.au.dk/for-applicants/apply-here/august-2019/phd-students-for-center-for-basic-research-in-program-verification/ Applications are received four times a year, next deadline is August 1, 2019. Best wishes, Lars — Lars Birkedal Villum Investigator, Professor Head of Logic and Semantics Group Department of Computer Science Aarhus University www.cs.au.dk/~birke birke...@cs.au.dk
[TYPES/announce] CFP FoSSaCS 2012
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CFP: 15th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) 2012, 24 March - 1 April. Tallinn, Estonia. http://itu.dk/research/fossacs-2012/ The submission site is now open! FoSSaCS seeks original papers on foundational research with a clear significance for software science. The conference invites submissions on theories and methods to support the analysis, integration, synthesis, transformation, and verification of programs and software systems. The specific topics covered by the conference include, but are not limited to, the following: Automata and language theory; Behavioural equivalences; Categorical models; Infinite state systems; Modal, spatial, and temporal logics; Models of concurrent, reactive, distributed, hybrid, and mobile systems; Process algebras and calculi; Semantics of programming languages; Software specification and refinement; Type systems and type theory; Fundamentals of security; Semi-structured data; Program correctness and verification. As a part of ETAPS, FoSSaCS adheres to ETAPS submission and notification deadlines, but FoSSaCS will also include an author response period: Friday, October 7, 2011 (23:59 Apia, Samoa time): Deadline for submission of abstracts. Friday, October 14, 2011, 23:59 Apia, Samoa time: Deadline for submission of full papers. Thursday and Friday, December 8-9, 2011:Author Response Friday, December 16, 2011: Notification of acceptance Friday, January 6, 2012:Camera-ready paper versions due March 24 - April 1, 2012: FoSSaCS 2012 Conference The paper submission deadline is STRICT. Making the deadline for submission of abstracts a week early allows the programme committee to start work before full versions are available. Obviously, there is no need to wait with submission of the full version until the final deadline. Submission of an abstract implies no obligation to submit a full version; abstracts with no corresponding full versions by the final deadline will be treated as withdrawn, but authors are strongly encouraged, in this case, to explicitly withdraw their submission by sending an e-mail to the chairman. Programme chair Lars Birkedal (IT Univ. of Copenhagen, Denmark) Invited speaker: Glynn Winskel (Univ. of Cambridge, UK) Programme committee: Luca Aceto (Reykjavik Univ., Iceland) Roberto Amadio (Univ. of Paris 7, France) Torben Amtoft (Kansas State Univ., USA) Lars Birkedal (IT Univ. of Copenhagen, Denmark) Mikolaj Bojanczyk (Warsaw University, Poland) Thierry Coquand (Chalmers Univ. of Technology, Sweden) Andrea Corradini (Univ. of Pisa, Italy) Volker Diekert (Univ. of Stuttgart, Germany) Maribel Fernandez (King's College London, UK) Kohei Honda (Queen Mary, Univ. of London, UK) Bart Jacobs (Radboud Univ. of Nijmegen, Netherlands) Joost-Pieter Katoen (RWTH Aachen, Germany) Olivier Laurent (ENS Lyon, France) Rupak Majumdar (Max Planck Inst. for Software Systems, Germany) Markus Müller-Olm (Univ. of Münster, Germany) Joachim Parrow (Uppsala Univ., Sweden) Duško Pavlović (Univ. of Oxford, UK) Hanne Riis Nielson (Technical Univ. of Denmark) Alex Simpson (Univ. of Edinburgh, UK) Carolyn Talcott (SRI International, USA) Yde Venema (Univ. of Amsterdam, Netherlands) Thomáš Vojnar (Brno University, Czech Republic) Websites: http://www.itu.dk/research/fossacs-2012/ http://www.etaps.org/2012/fossacs
[TYPES/announce] Associate Professors in Computer Science at Aarhus University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Please circulate the announcement below for tenured faculty positions here in Aarhus. Best wishes, Lars Birkedal (cs.au.dk/~birke<http://cs.au.dk/~birke>) Professor, Head of Logic and Semantics Group Associate Professors in Computer Science at Aarhus University One or more positions as associate professor are available at the Department of Computer Science, Aarhus University (www.cs.au.dk<http://www.cs.au.dk/>) starting January 1, 2014. The department has research groups within “Algorithms and Data Structures”, “Data-Intensive Systems”, “Cryptography and Security”, “Mathematical Computer Science”, “Logics and Semantics”, “Ubiquitous Computing and Interaction”, “Computer-Mediated Activity”, “Use, Design and Innovation”, “Programming Languages”, “Computer Graphics and Image Processing” and “Bioinformatics”. In addition, we want to build competences within “Software Engineering / Multicore/ Systems”, “Machine Learning / Data Mining” and “Quantum Informatics”. Applicants are expected to have several years of experience at the assistant professor level. They must document a strong record of original research and have teaching experience at undergraduate/graduate level. The department has a staff of 140 people including 28 full and associate professors, 5 assistant professors, 25 PostDocs and 65 PhD students. The number of students is approximately 1,000. Further information can be obtained from head of department Kurt Jensen (kjen...@cs.au.dk<mailto:kjen...@cs.au.dk>) or vice head of research Mogens Nielsen (m...@cs.au.dk<mailto:m...@cs.au.dk>). Please apply online at http://www.au.dk/en/job/nat/academicpositions/ before August 15, 2013.
[TYPES/announce] associate professor positions in Aarhus, Denmark
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear All, We have a call for new permanent positions at the Department of Computer Science, Aarhus University, with application deadline November 10. Applicants within the areas of ³Algorithms and Data Structures², ³Data-Intensive Systems², and ³Machine Learning² are of special interest, but we welcome strong applicants from other research areas as well. Would be great with strong applicants from the types community! Here is a short link to the official call text: http://tinyurl.com/kmpupck Please circulate this information to potential applicants. Thank you very much in advance, Lars -- Lars Birkedal Head of Department of Computer Science, Professor, Head of Logic and Semantics Group web: www.cs.au.dk/~birke email: birke...@cs.au.dk phone: +45 2383 8546
[TYPES/announce] Postdoc and PhD positions in Aarhus
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear Colleagues, We are looking for PhD students and postdocs in the area of Programming, Logic and Semantics, here at Aarhus University, Denmark. Several positions are available, in projects ranging from automated static and dynamic analysis of libraries and frameworks for web applications; theories and tools for language-based security; theories and tools for modular reasoning about higher-order concurrent imperative programs; and type theory and interactive proof assistants. Please circulate this announcement to potential applicants and encourage them to get in contact with one of us. Best wishes, Aslan Askarov (as...@cs.au.dk<mailto:as...@cs.au.dk>) Lars Birkedal (birke...@cs.au.dk<mailto:birke...@cs.au.dk>) Olivier Danvy (da...@cs.au.dk<mailto:da...@cs.au.dk>) Anders Møller (amoel...@cs.au.dk<mailto:amoel...@cs.au.dk>) Students interested in pursueing a PhD should apply at the Graduate School for Science and Technology http://talent.au.dk/phd/scienceandtechnology/ (next deadline May 1, 2015). They are encouraged to get in contact with one of us before applying. Potential postdocs should get in contact with us directly. Positions are typically for 2 years. Salary and working conditions for PhD students and postdocs are very competetive. — Lars Birkedal Head of Department of Computer Science, Professor Head of Logic and Semantics Group Department of Computer Science Aarhus University www.cs.au.dk/~birke<http://www.cs.au.dk/~birke> birke...@cs.au.dk<mailto:birke...@cs.au.dk>
[TYPES/announce] HOPE 2015 workshop @ ICFP - call for talk abstracts
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Reminder: Deadline for HOPE 2015 abstracts is on June 12, 2015 Details below. -- HOPE 2015 The 4th ACM SIGPLAN Workshop on Higher-Order Programming with Effects August 30, 2015 Vancouver, Canada (the day before ICFP 2015) http://users-cs.au.dk/birke/hope-2015/ HOPE 2015 aims at bringing together researchers interested in the design, semantics, implementation, and verification of higher-order effectful programs. It will be *informal*, consisting of invited talks, contributed talks on work in progress, and open-ended discussion sessions. - Goals of the Workshop - A recurring theme in many papers at ICFP, and in the research of many ICFP attendees, is the interaction of higher-order programming with various kinds of effects: storage effects, I/O, control effects, concurrency, etc. While effects are of critical importance in many applications, they also make it hard to build, maintain, and reason about one's code. Higher-order languages (both functional and object-oriented) provide a variety of abstraction mechanisms to help "tame" or "encapsulate" effects (e.g. monads, ADTs, ownership types, typestate, first-class events, transactions, Hoare Type Theory, session types, substructural and region-based type systems), and a number of different semantic models and verification technologies have been developed in order to codify and exploit the benefits of this encapsulation (e.g. bisimulations, step-indexed Kripke logical relations, higher-order separation logic, game semantics, various modal logics). But there remain many open problems, and the field is highly active. The goal of the HOPE workshop is to bring researchers from a variety of different backgrounds and perspectives together to exchange new and exciting ideas concerning the design, semantics, implementation, and verification of higher-order effectful programs. We want HOPE to be as informal and interactive as possible. The program will thus involve a combination of invited talks, contributed talks about work in progress, and open-ended discussion sessions. There will be no published proceedings, but participants will be invited to submit working documents, talk slides, etc. to be posted on this website. --- Call for Talk Proposals --- We solicit proposals for contributed talks. We recommend preparing proposals of at most 2 pages, in either plain text or PDF format. However, we will accept longer proposals or submissions to other conferences, under the understanding that PC members are only expected to read the first two pages of such longer submissions. When submitting talk proposals, authors should specify how long a talk the speaker wishes to give. By default, contributed talks will be 30 minutes long, but proposals for shorter or longer talks will also be considered. Speakers may also submit supplementary material (e.g. a full paper, talk slides) if they desire, which PC members are free (but not expected) to read. We are interested in talks on all topics related to the interaction of higher-order programming and computational effects. Talks about work in progress are particularly encouraged. If you have any questions about the relevance of a particular topic, please contact the PC chairs, Lars Birkedal (birke...@cs.au.dk) and Neel Krishnaswami (n.krishnasw...@cs.bham.ac.uk). Deadline for talk proposals:June 12, 2015 (Friday) Notification of acceptance: July 3, 2015 (Friday) Workshop:August 30, 2015 (Sunday) The submission website is now open: https://www.easychair.org/conferences/?conf=hope2015 --- Invited Speaker --- Aaron Turon, Mozilla - Workshop Organization ----- Program Co-Chairs: Lars Birkedal (Aarhus University) Neel Krishnaswami (University of Birmingham) Program Committee: Viviana Bono (Università di Torino) Pierre Clairambault (ENS Lyon) Mike Dodds (University of York) Naoki Kobayashi (University of Tokyo) Sam Lindley (University of Edinburgh) Rasmus Møgelberg (IT University of Copenhagen) Tahina Ramananandro (Reservoir Labs Inc.) Kasper Svendsen (Aarhus University) Nikos Tzevelekos (Queen Mary University) Nobuko Yoshida (Imperial College) Noam Zeilberger (MSR-Inria)
[TYPES/announce] Call for Participation - Iris Workshop 2019 - Aarhus Univ - October 28-29, 2019
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Call for Participation - Iris Workshop 2019 Aarhus University - October 28-29, 2019 Dear All, On October 28-29, we are hosting the Iris Workshop 2019 at the Department of Computer Science, Aarhus University. It is a specialist workshop focusing on Iris-related research, but we welcome participation by anyone who is interested. Find more information about the workshop here: https://iris-project.org/workshop-2019/ and find out more about Iris here: https://iris-project.org Participation in the workshop is free, but you need to register your participation at https://events.au.dk/iris2019 (deadline: October 11). All participants are welcome to stay 1-3 days longer for more informal discussions and interaction. PRELIMINARY PROGRAM: October 28 09:00 - 10:00: Invited talk: Ralf Jung: Logical Atomicity in Iris: The Good, the Bad, and the Ugly 10:00 - 10:30: Coffee break 10:30 - 11:00: Amin Timany: Aneris: A Logic for Node-Local, Modular Reasoning of Distributed Systems 11:00 - 11:30: Jesper Bengtson: Actris: Session-Type Based Reasoning in Separation Logic 11:30 - 12:00: Rodolphe Lepigre: TBA 12:00 - 13:30: Lunch 13:30 - 14:30: Invited Talk: François Pottier: Playing spy games in Iris 14:30 - 15:00: Léo Stefanesco: TBA 15:00 - 15:30: Coffee and cake 15:30 - 16:00: Philippa Gardner: Compositional Reasoning for the Termination of Fine-grained Concurrent Programs 16:00 - 17:00: Invited Talk: Gregory Malecha: TBA 18:30 - 21:30: Conference dinner at No. 16 (https://no16.nu/) October 29 09:00 - 10:00: Invited talk: Dan Frumin: Compositional Non-Interference for Fine-Grained Concurrent Programs 10:00 - 10:30: Coffee break 10:30 - 11:00: Glen Mével: Iris for Multicore OCaml 11:00 - 11:30: Armaël Guéneau: Formal verification of an incremental cycle detection algorithm 11:30 - 12:00: Andrew Appel: Recent developments in the Verified Software Toolchain 12:00 - 13:30: Lunch 13:30 - 14:30: Invited Talk: Bart Jacobs: Specifying I/O using Abstract Nested Hoare Triples 14:30 - 15:00: Aïna Linn Georges: Implementing a Capability Machine model into Iris 15:00 - 15:30: Coffee and cake 15:30 - 16:00: Paolo Giarrusso: Step-Indexed Logical Relations for (guarded) Dependent Object Types 16:00 - 16:30: Hai Dang: RustBelt Relaxed Best wishes, Robbert Krebbers and Lars Birkedal -- Lars Birkedal Villum Investigator Professor, Head of Logic and Semantics Group Dept. of Computer Science Aarhus University Aabogade 34 8200 Aarhus N Denmark birke...@cs.au.dk<mailto:birke...@cs.au.dk> www.cs.au.dk/~birke
[TYPES/announce] PhD and Postdoc positions in Aarhus (Denmark)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Department of Computer Science at Aarhus University, Denmark, offers a considerable number of PhD and PostDoc positions in the areas of Logic, Semantics and Programming Languages. Our research spans a wide spectrum of topics concerning models and logics for programming languages and type theories, language-based security, blockchains, theoretical foundations and practical tools for program analysis, formal verification and model checking. Aarhus University admits PhD students on the basis of a bachelor's degree (for 5 year PhDs) or a master's degree (for 3 year PhDs). If admitted, all tuition is covered, and a generous stipend is provided. Postdoc positions can be for 1 or 2 years, and with the possibility of renewal (depending on the individual projects and sources of funding). Interested applicants at all levels are encouraged to contact the respective faculty for details, enclosing a CV and a short description of interests. Logic and Semantics group: http://cs.au.dk/research/logic-and-semantics/ - Aslan Askarov (language-based security, web security, type systems, program analysis) - Lars Birkedal (higher-order concurrent separation logic, type theory, program verification) - Bas Spitters (computer aided proofs in cryptography, homotopy type theory, formal verification of blockchains) - Jaco van de Pol (parallel & symbolic model checking, synthesis, graph games) Programming Languages group: https://cs.au.dk/research/programming-languages/ - Magnus Madsen (programming language design, functional and logic programming, type systems) - Anders Møller (static & dynamic program analysis, program analysis and automated testing for web and mobile software) - Andreas Pavlogiannis (algorithmic & computational foundations of model checking, quantitative verification, static & dynamic analysis, concurrency) Aarhus University is realizing an ambitious multi-phase digitalization initiative which will help prepare researchers, students and the labour force for the digital transition of the future. The initiative aims at significant expansion of the Department of Computer Science for faculty and students. Next deadline: November 1st, 2019 Information about the PhD program: http://phd.scitech.au.dk/for-applicants/application-guide/ -- Lars Birkedal Villum Investigator Professor, Head of Logic and Semantics Group Dept. of Computer Science Aarhus University Aabogade 34 8200 Aarhus N Denmark birke...@cs.au.dk<mailto:birke...@cs.au.dk> www.cs.au.dk/~birke
[TYPES/announce] postdoc position in Aarhus, Denmark, at Center for Basic Research in Program Verification
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are looking for Postdocs to work in the Center for Basic Research in Program Verification in Aarhus, Denmark. Research topics include: extensions of higher-order concurrent separation logics (such as our Iris logic, see iris-project.org), e.g., to reason about distributed systems; probabilistic program logics; logical relations for relational reasoning about safety and security properties; formal modeling of low-level capability machines, and secure compilation; guarded cubical type theory; and Coq formalizations. The Post Doc positions are for two years (with a possibility of extension). Application deadline is June 1, 2020. See https://www.au.dk/om/stillinger/job/center-for-basic-research-in-program-verification-cpv-is-looking-for-postdocs/ for more information. Please contact me at birke...@cs.au.dk<mailto:birke...@cs.au.dk> if you have any questions. Best wishes, Lars Birkedal -- -- Lars Birkedal Villum Investigator Professor, Head of Logic and Semantics Group Dept. of Computer Science Aarhus University Aabogade 34 8200 Aarhus N Denmark birke...@cs.au.dk<mailto:birke...@cs.au.dk> www.cs.au.dk/~birke<http://www.cs.au.dk/~birke>
[TYPES/announce] Assoc. Professorship Opening
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Associate Professorship in Programming, Logic and Semantics at the IT University of Copenhagen, Denmark. The IT University of Copenhagen invites applications for a position as Associate Professor in the Programming, Logic, and Semantics Group. The position is available from August 2007. The Programming, Logic and Semantics (PLS) group at the IT University of Copenhagen conducts research in semantics of logics and programming languages; models for concurrent, mobile and distributed systems; logical frameworks, modular software verification; programming language implementation techniques; program analysis; and programming language technology for distributed and mobile applications, in particular for context-aware mobile computing. The successful candidate must document internationally recognized research in the research areas of the PLS group. Moreover, the applicant should be willing and able to teach in a wide variety of courses at all levels. Please see http://www1.itu.dk/sw58262.asp for the full official announcement. Application deadline is April 16, 2007. Best wishes, Lars Birkedal
[TYPES/announce] positions at the IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The IT University of Copenhagen invites applications for six (6) assistant/associate professorships starting December 2007. Application deadline is September 3, 2007. Please see http://www1.itu.dk/sw64250.asp for details. Best wishes, Lars Birkedal
[TYPES/announce] Ph.D. scholarships at the IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] A number of Ph.D. scholarships are available at the IT University of Copenhagen, including some in the areas of the Programming, Logic and Semantics (PLS) Group with research in programming languages, automated reasoning, logical frameworks, type theory, semantics, category theory, domain theory, distributed and mobile computing, business processes, concurrency theory, electronic voting. Please let potential students know. Deadline for application is October 22. See http://www1.itu.dk/sw66047.asp for the official announcement. Best wishes, Lars Birkedal Head of the PLS group.
[TYPES/announce] Assoc. Prof. position at IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The IT University of Copenhagen invites applications for a tenured position as Associate Professor starting March 1, 2008 in the Programming, Logic and Semantics (PLS) group. The Programming, Logic and Semantics (PLS) group at the IT University of Copenhagen conducts research in the semantics of logics and programming languages; models for concurrent, mobile and distributed systems; logical frameworks, modular software verification; programming language implementation techniques; program analysis; and programming language technology for distributed and mobile applications, in particular for context-aware mobile computing. Application deadline is Nov. 12, at noon. Please see http://www1.itu.dk/sw70441.asp for the full official announcement. Best wishes, Lars Birkedal
[TYPES/announce] Ph.D. school on Logics and Semantics of State
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Please circulate the following announcement to Ph.D. students. Thanks, Lars Birkedal. Call for Participation FIRST PhD Fall School on Logics and Semantics of State IT University of Copenhagen, Denmark October 20-24, 2008 <http://itu.dk/people/kss/fall-school-2008/> Background The Fall School on Logics and Semantics of State will cover current research focused on developing logics for reasoning modularly about programs with state. Speakers will present material covering separation logic, certified systems software, modular verification methodologies for object-oriented programs, and separation logic for object-oriented and higher-order programs. Both foundations and applications will be covered in the lectures. Material will be presented at a tutorial level that will help graduate students (advanced M.Sc. students and Ph.D. students) and researchers from academia or industry get an overview of state-of-the-art techniques and understand open problems confronting the field. The Fall school is open to anyone interested. Prerequisites are an elementary knowledge of logic and mathematics that is usually covered in undergraduate classes on discrete mathematics. Some knowledge of programming languages at the level provided by a beginning graduate survey course will also be expected. Our primary target group consists of advanced M.Sc. students, Ph.D. students, and post-doctoral researchers. Lecturers and topics John C. ReynoldsSeparation Logic - A Logic for Shared Data and Local Reasoning Zhong Shao Modular Development of Certified System Software David Naumann Modular Specification and Verification of Object-oriented Programs Matthew Parkinson Separation Logic for Object-oriented Programs Lars Birkedal and Hongseok Yang Separation Logic for Higher-order Programs For more information about the contents, see the Fall school web site: <http://itu.dk/people/kss/fall-school-2008/> Time and place The Fall school will take place at the IT University of Copenhagen from October 20 to October 24 (Monday through Friday). Each topic will be covered by seven hours of lectures and exercises during the week. Registration To register for the Fall school, please send an email to [EMAIL PROTECTED] no later than *** Friday, September 19. *** The email should contain your name and affiliation. If you are a student, your supervisor (or another faculty member) must in addition send a brief letter of support by email to the same address. The registration fee is 500 DKK / Euro 65, covering course materials, coffee, and lunches. The fee does not cover accommodation. Information about payment methods will be announced. FIRST PhD students participate free of charge. Organization The Fall school is sponsored by the FIRST Research School. Organizers: Lars Birkedal and Kristian Stoevring, IT University of Copenhagen.
[TYPES/announce] assoc. prof. opening at IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The IT University of Copenhagen invites applications for an associate professorship in software development. The official announcement can be found at http://www1.itu.dk/graphics/ITU-library/Intranet/Personale/Stillingsopslag/VIP/Stillingsopslag%202009/Lektor%20SDG%20-%202009-223-0007.pdf Application deadline is 12:00 on February 12, 2009. Best wishes, Lars Birkedal. The research interests of the applicant should preferably be within software development, programming languages, or systems. This includes requirements specification, decision support systems, programming language technology including program analysis, database technology, model-driven development, end-user development, software development processes, software architecture, models and technology for concurrent and mobile systems, modular software verification, models and technology for ubiquitous computing, and IT for healthcare.
[TYPES/announce] Two post. doc. positions - Tools and Methods for Scalable Software Verification
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We have two two-year post. doc. positions in our recently-funded project on Tools and Methods for Scalable Software Verification at the IT University of Copenhagen, Denmark. The goals of the project are (A) to apply advances in separation logic to the specification and proof of programs in current languages, such as Java and C#, that combine references, shared state and destructive update; (B) to develop prototype software tools for formal specification and apply them in a substantial real-life case study; and (C) to give methodological advice on how to structure software so as to facilitate formal specification and proof. Please see http://www1.itu.dk/graphics/ITU-library/Intranet/Personale/Stillingsopslag/VIP/Stillingsopslag%202009/Post%20doc%202009_05.pdf for the official announcement. Application deadline: June 15, 12:00. [The project will, in part, be done in collaboration with M. Parkinson (Univ. of Cambridge) and D. Distefano (Queen Mary, Univ. of London). The project is related to the ongoing MoReaSo project at the IT University of Copenhagen (see http://www.itu.dk/people/birkedal/moreaso/).] Please contact Lars Birkedal (birke...@itu.dk) or Peter Sestoft (sest...@itu.dk) for more information. Best wishes, Lars Birkedal - Lars Birkedal Professor, Head of Programming, Logic, and Semantics Group IT University of Copenhagen Web: http://www.itu.dk/people/birkedal Phone: +45 7218 5280 Email: birke...@itu.dk
[TYPES/announce] Ph.D. scholarships at the IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear All, A number of Ph.D. positions are available in the FIRST research school at the IT University of Copenhagen. The FIRST research school covers theoretical computer science and fundamental software technologies. Please see http://www1.itu.dk/sw487.asp for the official announcement and for information on how to apply. Application deadline is October 7, 2009. Potential applicants are welcome to contact me or any of the other faculty members in the PLS group (www.itu.dk/research/pls) for more information. Best wishes, Lars Birkedal Professor, Head of PLS group and the FIRST research school. www.itu.dk/~birkedal
[TYPES/announce] Ph.D. positions at the IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear All, A number of Ph.D. positions are available in the Programming, Logic, and Semantics research group at the IT University of Copenhagen. Please see http://www1.itu.dk/graphics/ITU-library/Intranet/Personale/Stillingsopslag/VIP/Stillingsopslag%202010/PhD%20call_spring%202010_text.pdf for the official announcement and for information on how to apply. Application deadline is March 24, 2010. Potential applicants are welcome to contact me or other faculty members in the PLS group (www.itu.dk/research/pls) for more information. Best wishes, Lars Birkedal Professor, Head of PLS group and the FIRST research school. www.itu.dk/~birkedal
[TYPES/announce] Assistant or Associate Professors of Computer Science
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Assistant or Associate Professorships in Computer Science at the IT University of Copenhagen, Denmark. We are inviting applications for Assistant / Associate Professorships at the IT University of Copenhagen, in particular in the areas of Programming, Logic, and Semantics. Application deadline is February 16, 2011. Please see https://delta.hr-manager.net/ApplicationInit.aspx?ProjectId=79841&DepartmentId=5237&MediaId=1282 for the official annoucement. Potential applicants are welcome to contact me for further information. Best wishes, Lars Birkedal birke...@itu.dk ----- Lars Birkedal Professor, Head of Programming, Logic, and Semantics Group IT University of Copenhagen Web: http://www.itu.dk/people/birkedal Phone: +45 7218 5280 Email: birke...@itu.dk
