[TYPES/announce] Postdoc position at IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, I would like to advertise a 2-year postdoc position available at the IT University of Copenhagen, Denmark. The suggested starting date is August 2017, but this is negotiable. The position is part of my research project Type Theories for Reactive Programming funded by Villum Fonden, and running for 5 years involving 2 PhDs and 2 postdoc positions in total. I include a short description of the goals of the project below. Applicants should have experience with category theory and denotational semantics. Knowledge of models of (dependent) type theory or functional reactive programming is an advantage, but is not required. The deadline for application is February 28. Further information on the position and how to apply can be found here: http://bit.ly/2kl7zRy I encourage all interested in applying to contact me in advance. Rasmus Møgelberg - Project description Type theories are formal systems that can be viewed both as programming languages and logical systems for formalised mathematics. From a computer science perspective, this is useful because it allows for programs, their specifications, and the proofs that these satisfy the specification to be expressed in the same formalism. The logical interpretation of type theories means that all programs must terminate. For this reason, programming and reasoning about non-terminating reactive programs in type theory remains a challenge. This is unfortunate since these include many of the most critical programs in use today. In this project, we aim to design a new type theory useful for programming with and reasoning about reactive programs. We build on recent progress in guarded recursion and functional reactive programming, using modalities to capture productivity in types. The project also involves the development of Guarded Cubical Type Theory, an extension of Cubical Type Theory with guarded recursive types. These can be used for smooth programming with coinductive types and construction of models of advanced programming languages. This part of the project is a collaboration with professor Lars Birkedal at Aarhus University. Type theories are formal systems that can be viewed both as programming languages and logical systems for formalised mathematics. From a computer science perspective, this is useful because it allows for programs, their specifications, and the proofs that these satisfy the specification to be expressed in the same formalism. The logical interpretation of type theories means that all programs must terminate. For this reason, programming and reasoning about non-terminating reactive programs in type theory remains a challenge. This is unfortunate since these include many of the most critical programs in use today. In this project, we aim to design a new type theory useful for programming with and reasoning about reactive programs. We build on recent progress in guarded recursion and functional reactive programming, using modalities to capture productivity in types. The project also involves the development of Guarded Cubical Type Theory, an extension of Cubical Type Theory with guarded recursive types. These can be used for smooth programming with coinductive types and construction of models of advanced programming languages. This part of the project is a collaboration with professor Lars Birkedal at Aarhus University. - See more at: https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119=180828=5#sthash.uggmBukd.dpu Project description Type theories are formal systems that can be viewed both as programming languages and logical systems for formalised mathematics. From a computer science perspective, this is useful because it allows for programs, their specifications, and the proofs that these satisfy the specification to be expressed in the same formalism. The logical interpretation of type theories means that all programs must terminate. For this reason, programming and reasoning about non-terminating reactive programs in type theory remains a challenge. This is unfortunate since these include many of the most critical programs in use today. In this project, we aim to design a new type theory useful for programming with and reasoning about reactive programs. We build on recent progress in guarded recursion and functional reactive programming, using modalities to capture productivity in types. The project also involves the development of Guarded Cubical Type Theory, an extension of Cubical Type Theory with guarded recursive types. These can be used for smooth programming with coinductive types and construction of models of advanced programming languages. This part of the project is a collaboration with professor Lars Birkedal at Aarhus University. - See more at:
[TYPES/announce] Workshop DaLí
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Workshop DaLí – Dynamic Logic: new trends and applications Brasília, 24 September, 2017 (co-located with FROCOS TABLEAUX and ITP 2017) workshop.dali.di.uminho.pt Building on the pioneer intuitions of Floyd-Hoare logic, Dynamic Logic was intro- duced in the 70’s by Pratt as a suitable logic to reason about, and verify, classic imperative programs. Since then, the original intuitions grew to an entire family of logics, which became increasingly popular for assertional reasoning about a wide range of computational systems. Simultaneously, their object (i.e. the very notion of a program) evolved in unexpected ways. This leads to dynamic logics tailored to specific programming paradigms and extended to new computing domains, including probabilistic, continuous and quantum computation. Both its theoretical relevance and practical potential make Dynamic Logic a topic of interest in a number of scientific venues, from wide-scope software engineering conferences to modal logic specific events. However, no specific event is exclusively dedicated to it. This workshop aims at filling fill such a gap, joining an heteroge- neous community of colleagues, from Academia to Industry, from Mathematics to Computer Science. forum for disseminating and sharing new trends and applications of Dynamic Logic. The event is promoted by the project DaLí - Dynamic logics for cyber-physical systems: towards contract based design (POCI-01-0145-FEDER-016692), a R project supported by the Portuguese Foundation for Science and Technology (http: //dali.di.uminho.pt). * Topics * We invite submissions on the general field of Dynamic Logic, its variants and applications, including, but not restricted to: - Dynamic logic,foundations and applications - Logics with regular modalities - Modal/temporal/epistemic logics - Kleene and action algebras and their variants - Quantum dynamic logic - Coalgebraic modal/dynamic logics - Graded and fuzzy dynamic logics - Dynamic logics for cyber-physical systems - Dynamic epistemic logic - Complexity and decidability of variants of dynamic logics and temporal logics - Model checking, model generation and theorem proving for dynamic logics * Submissions and publications Authors are invited to submit original papers (un-published and not submitted for publication elsewhere) up to 15 pages in lncs style. Accepted papers will be published in a Springer’s Lecture Notes of Computer Science volume. Submissions with work in progress (abstracts with 2-5 pag) are also welcomed for short presentations. They are subject of a light reviewing and will be available at conference in a informal booklet. Both kind of submissions should be done via the EasyChair link https://easychair.org/conferences/?conf=dali17. Extended versions of the DaLí contributions will be invited to a special issue in the Journal of Logical and Algebraic Methods in Programming, Elsevier. * Important Dates - May 26, 2017: Abstract deadline - June 2, 2017: Full paper deadline - July 14, 2017: Author notification Invited Speakers - Alexandru Baltag, UVA, NL - Edward Hermann Haeusler, PUC-Rio, BR PC Chairs - Alexandre Madeira (UM & UA, PT) - Mário Benevides (UFRJ, BR) Program Committee: - Carlos Areces (U. Cordoba, AR) - Phillippe Balbiani (U. Toulouse, FR) - Alexandru Baltag (Uva, NL) - Luís S. Barbosa (U.Minho, PT) - Johan van Benthem (U.Stanford & U.Tsinghua) - Patrick Blackburn (U. Roskilde, DK) - Stéphane Demri (ENS Cachan, FR) - Hans van Ditmarsch (LORIA, Nancy, FR) - Francicleber M. Ferreira (UFC, BR) - Valentin Goranko (U. Stockholm, SE) - Edward H. Hauesler (PUC-Rio, BR) - Rolf Hennicker (LMU, Munchen, DE) - Andreas Herzig (Toulouse, FR) - Dexter Kozen (Cornell, USA) - Clemens Kupke (U.Strathclyde, UK) - Bruno Vieira Lopes (UFF, BR) - Paulo Mateus (IST, PT) - Manuel A. Martins (U.Aveiro, PT) - Carlos Olarte (UFRN, BR) - José N. Oliveira (U. Minho, PT) - André Platzer (CMU, USA) - Eugénio Rocha (U. Aveiro, PT) - Valéria de Paiva (NC, USA) - Regivan Santiago (UFRN, BR) - Luis Menasche Schechter (UFRJ, BR) - Alexandra Silva (UCL, UK) - Tinko Tinchev (U. Sofia, BG) - Petrucio Viana (UFF, BR) - Yde Venema (ILLC, NL) - Renata Wassermann (USP, BR)
[TYPES/announce] SAS 2017 - First Call For Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] -- SAS 2017 24th Static Analysis Symposium New York City, NY, August 30th-September 1st, 2017 http://staticanalysis.org/sas2017 -- OBJECTIVE Static Analysis is widely recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. The series of Static Analysis Symposia has served as the primary venue for the presentation of theoretical, practical, and application advances in the area. The 24th International Static Analysis Symposium, SAS 2017, will be held at New York University, New York City, NY, USA. Previous symposia were held in Edinburgh, Saint-Malo, Munich, Seattle, Deauville, Venice, Perpignan, Los Angeles, Valencia, Kongens Lyngby, Seoul, London, Verona, San Diego, Madrid, Paris, Santa Barbara, Pisa, Aachen, Glasgow, and Namur. TOPICS The technical program for SAS 2017 will consist of invited lectures and presentations of refereed papers. Contributions are welcomed on all aspects of static analysis, including, but not limited to: - Abstract domains - Abstract interpretation - Automated deduction - Data flow analysis - Debugging - Deductive methods - Emerging applications - Model checking - Program optimization and transformation - Program synthesis - Program verification - Security analysis - Tool environments and architectures - Theoretical frameworks - Type checking PAPER SUBMISSION Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic, object-oriented, aspect, multi-core, distributed, and GPU programming. Papers must describe original work, be written and presented in English, and must not substantially overlap with papers that have been published or that are simultaneously submitted to a journal or a conference with refereed proceedings. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should clearly identify what has been accomplished and why it is significant. Paper submissions should not exceed 18 pages in Springer's Lecture Notes in Computer Science LNCS format, excluding bibliography and well-marked appendices. Program Committee members are not required to read the appendices, and thus papers must be intelligible without them. Submissions are handled online through easychair: https://easychair.org/conferences/?conf=sas2017 ARTIFACT SUBMISSION As in previous years, we are encouraging authors to submit a virtual machine image containing any artifacts and evaluations presented in the paper. The goal of the artifact submissions is to strengthen our field's scientific approach to evaluations and reproducibility of results. The virtual machines will be archived on a permanent Static Analysis Symposium website to provide a record of past experiments and tools, allowing future research to better evaluate and contrast existing work. Artifact submission is optional. We accept only virtual machine images that can be processed with Virtual Box. Details on what to submit and how will be sent to the corresponding authors by mail shortly after the paper submission deadline. The submitted artifacts will be used by the program committee as a secondary evaluation criteria whose sole purpose is to find additional positive arguments for the paper's acceptance. Submissions without artifacts are welcome and will not be penalized. IMPORTANT DATES - Abstract submission: April 14, 2017 (anywhere on earth) - Full paper submission: April 20, 2017 (anywhere on earth) - Artifact submission: April 25, 2017 (anywhere on earth) - Author notification: June 12, 2017 - Final version due: July 5, 2017 - Conference: August 30 - September 1, 2017 CONFERENCE VENUE The conference will be held in the Forbes Building of the New York University, 60 Fifth Avenue, New York City. RADHIA COUSOT AWARD Since 2014, the program committee of each SAS conference selects a paper for the Radhia Cousot Young Researcher Best Paper Award, in memory of Radhia Cousot, and her fundamental contributions to static analysis, as well as being one of the main promoters and organizers of the SAS series of conferences. SPECIAL ISSUE Full versions of a selection of accepted papers, to be determined by the program committee, will be invited for submission to Formal Methods in System Design journal. INVITED SPEAKERS Alex Aiken (Stanford University, USA) Francesco Logozzo (Facebook, USA) Peter Müller (ETH Zurich, Switzerland) AFFILIATED EVENTS - NSAD: The 7th Workshop on Numerical and Symbolic Abstract Domains - SASB: The 8th Workshop on Static Analysis
[TYPES/announce] Logic Colloquium 2017: First Announcement and Call for Submissions
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Logic Colloquium 2017: First Announcement and Call for Submissions August 14-20, 2017, Stockholm, Sweden https://www.lc17.conf.kth.se The Logic Colloquium 2017 (LC2017) is the 2017 Annual European summer meeting of the Association for Symbolic Logic (ASL) and will be held during August 14-20, 2017 at the main campus of Stockholm University. The Logic Colloquium 2017 is organised and hosted jointly by the Departments of Mathematics and Philosophy at Stockholm University, and is also supported by the KTH Royal Institute of Technology. LC2017 will be co-located with two other logic-related events, all taking place at Stockholm University: - the 3rd Nordic Logic Summer School, NLS2017, August 7-12 - the 26th EACSL Annual Conference on Computer Science Logic, CSL2017, August 20-24. There will be a joint session of CSL2017 and LC2017 in the morning of August 20. Further information about all events can be found at: https://www.lis17.conf.kth.se The programme of LC2017 will also include special sessions, which will be announced later. INVITED SPEAKERS -- Plenary speakers: - David Aspero (University of East Anglia) - Alessandro Berarducci (Pisa) - Elisabeth Bouscaren (Paris 11) - Christina Brech (Sao Paulo) - Sakae Fuchino (Kobe University) - Denis Hirschfeldt (University of Chicago) - Wilfrid Hodges (British Academy) - Emil Jerabek (Prague) - Per Martin-Löf (Stockholm University) - Dag Prawitz (Stockholm University) - Sonja Smets (University of Amsterdam) Tutorial speakers: - Patricia Bouyer-Decitre (LSV ENS Cachan) - Mai Gehrke (Paris 7) LC2017 invited highlight speakers for the joint LC-CSL session: - Veronica Becher (Buenos Aires) - Pierre Simon (UC Berkeley) SUBMISSIONS OF CONTRIBUTED TALKS - Abstracts of contributed talks must be submitted as pdf files via this EasyChair page: https://easychair.org/conferences/?conf=lc2017 (If you do not have an EasyChair-account yet, you can create one at the submission site.) The abstracts must be prepared according to the ASL instructions here: http://www.aslonline.org/rules_abstracts.html Please enter Title and Abstract as plain text. As the first keyword, put the AMS 2010 classification: 03xxx Abstracts of contributed talks submitted by ASL members, which are accepted and prepared according to the ASL Rules for Abstracts will be published in The Bulletin of Symbolic Logic. Upon notification of acceptance, authors will be requested to submit the LaTex source files. ASL will provide some student grants for participation at the LC2017. IMPORTANT DATES Abstract submission for contributed talks: May 5, 2017 Notification: TBA PROGRAMME COMMITTEE --- - Rod Downey (University of Wellington) - Mirna Dzamonja (PC chair, University of East Anglia) - Ali Enayat (University of Gothenburg) - Fernando Ferreira (University of Lisbon) - Valentin Goranko (Stockholm University) - Martin Hils (University of Münster) - Sara Negri (University of Helsinki) - Assaf Rinot (Bar-Ilan University) - Igor Walukiewicz (University of Bordeaux) ORGANISING COMMITTEE - Mads Dam, Department of Theoretical Computer Science, KTH - Valentin Goranko (OC co-chair), Department of Philosophy, Stockholm University - Sven-Ove Hansson, Department of Philosophy, KTH Royal Institute of Technology - Eric Johannesson, Department of Philosophy, Stockholm University - Vera Koponen, Department of Mathematics, Uppsala University - Roussanka Loukanova, Department of Mathematics, Stockholm University - Peter LeFanu Lumsdaine, Department of Mathematics, Stockholm University - Peter Pagin, Department of Philosophy, Stockholm University - Anders Lundstedt, Department of Philosophy, Stockholm University - Erik Palmgren (OC co-chair), Department of Mathematics, Stockholm University - Dag Westerståhl, Department of Philosophy, Stockholm University CONTACTS AND ENQUIRIES For enquiries on scientific and programme issues, send email to: Mirna Dzamonja (m.dzamo...@uea.ac.uk) For enquiries on organising matters, send email to: lc2017 at philosophy.su.se
[TYPES/announce] Call for International Conference for Computational Semantics (IWCS) Workshop Proposals
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR IWCS WORKSHOP PROPOSALS 12th International Conference on Computational Semantics (IWCS) LIRMM & Universite de Montpellier, France 20th-22nd September 2017 (workshops on 19th) http://www.lirmm.fr/iwcs2017/workshops/index.html Proposal deadline: 10th February 2017 The International Conference for Computational Semantics (IWCS) invites proposals for one-day or half-day workshops, to be held in conjunction with the 2017 IWCS conference. IWCS 2017 will take place on 20th-22nd September 2017 at LIRMM, Universite de Montpellier, France. Workshops will take place on the day immediately preceding the conference: 19th September 2017. The aim of the IWCS conference is to bring together researchers interested in any aspects of the computation, annotation, extraction, and representation of meaning in natural language, whether this is from a lexical or structural semantic perspective. IWCS embraces both symbolic and statistical approaches to computational semantics, and everything in between. TOPICS OF INTEREST Topics of interest for the workshops include all subdomains of computational semantics relevant to the main conference, including but not limited to: - representation of meaning - syntax-semantics interface - representing and resolving semantic ambiguity - shallow and deep semantic processing and reasoning - hybrid symbolic and statistical approaches to representing semantics - alternative approaches to compositional semantics - inference methods for computational semantics - recognizing textual entailment - deep learning and semantics - learning by reading - methodologies and practices for semantic annotation - machine learning of semantic structures - statistical semantics - computational aspects of lexical semantics - semantics and ontologies - semantic web and natural language processing - semantic aspects of language generation - semantic relations in discourse and dialogue - semantics and pragmatics of dialogue acts - multimodal and grounded approaches to computing meaning - semantics-pragmatics interface SUBMISSION INFORMATION Proposals for workshops should contain: - A title and brief (2-page max) description of the workshop topic and content. - An estimate of the audience size. - The names, postal addresses, and email addresses of the organizers, with one-paragraph statements of their research interests and areas of expertise. - A list of potential members of the program committee, with an indication of which members have already agreed. - A description of special requirements for technical needs. Proposals should be submitted by email to iwcs2...@gmail.com as soon as possible, but no later than 10th February 2017. Notification of acceptance of workshop proposals will occur no later than 17th February 2017. AFTER ACCEPTANCE Organizers of accepted workshops must provide descriptions of their workshops, for inclusion in the conference registration material, by 1st April 2017. The description must be provided in two formats: an ASCII version that can be included with the email announcement, and an HTML version that can be included on the conference home page. These descriptions should be mailed to: iwcs2...@gmail.com The final workshop materials must be received by the IWCS organizers by 4th September 2017. This includes the detailed proceedings (camera-ready versions of papers), which will be made available electronically, as well as a short workshop program, which will be printed together with the main conference program. FINANCES Workshops must be financially self-supporting. The IWCS organizers will establish registration rates so as to provide the room, audio-visual equipment, internet access, snacks for breaks, and the workshop proceedings. IMPORTANT DATES 10th February 2017 Workshop proposal submissions due 17th February 2017 Workshop proposal notification of acceptance 1st April 2017 Workshop description mailed to IWCS organizers 4 September 2017 Workshop material due to IWCS organizers 19th September 2017 Workshop date
