[TYPES/announce] ProWeb 2017: 1st International Workshop on Programming Technology for the Future Web
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] ProWeb 2017: 1st International Workshop on Programming Technology for the Future Web http://2017.programming-conference.org/track/proweb-2017-papers Co-located with the conference April 3, Brussels, Belgium Full-fledged web applications have become ubiquitous on desktop and mobile devices alike. Whereas "responsive" web applications already offered a more desktop-like experience, there is an increasing demand for "rich" web applications (RIAs) that offer collaborative and even off-line functionality -Google docs being the prototypical example. Long gone are the days that web servers merely had to answer incoming HTTP request with a block of static HTML. Today's servers react to a continuous stream of events coming from JavaScript applications that have been pushed to clients. As a result, application logic and data is increasingly distributed. Traditional dichotomies such as "client vs. server" and "offline vs. online" are fading. ** Call for Papers ** The 1st International Workshop on Programming Technology for the Future Web, or ProWeb17, is a forum for researchers and practitioners to share and discuss new technology for programming these and future evolutions of the web. We welcome submissions introducing programming technology (i.e., frameworks, libraries, programming languages, program analyses and development tools) for implementing web applications and for maintaining their quality over time, as well as experience reports about the use of state-of-the-art programming technology. Relevant topics include, but are not limited to: * Quality on the new web: static and dynamic program analyses; code, design test and process metrics; development and migration tools; automated testing and test generation; contract systems, type systems, and web service API conformance checking; ... * Hosting languages on the web: new runtimes; transpilation or compilation to JavaScript, WebAssembly, asm.js, ... * Designing languages for the web: multi-tier (or tierless) programming; reactive programming; frameworks for multi-tier or reactive programming on the web; ... * Distributed data sharing, replication and consistency: cloud types, CRDTs, eventual consistency, offline storage, peer-to-peer communication, ... * Security on the web: client-side and server-side security policies; policy enforcement; proxies and membranes; vulnerability detection; dynamic patching, ... * Surveys and case studies using state-of-the-art web technology * Ideas on and experience reports about: how to reconcile the need for quality with the need for agility on the web; how to master and combine the myriad of tier-specific technologies required to develop a web application, .. * Position statements on what the future of the web should look like We solicit three kinds of submissions via EasyChair: https://easychair.org/conferences/?conf=proweb2017 - 6-page **technical papers** and **experience reports** that, when accepted, will be published in the workshop post-proceedings as part of of the ACM's Digital Library. - 3-page **position statements** that, when accepted, will be published in the workshop post-proceedings as part of of the ACM's Digital Library. - 1-page **presentation abstracts** that, when accepted, will be made available on the website. Submissions must follow the ACM SIGPLAN Conference Format (9 point font, Times New Roman font family, numeric citation style). Each submission will be reviewed by at least three members of the program committee. We welcome submissions that identify new problems, or report on promising ideas in early stages of research. Submissions of the third kind are ideal to further disseminate existing ideas within the community, to demonstrate existing tools, or simply to instigate a discussion. More information: http://2017.programming-conference.org/track/proweb-2017-papers ** Important dates (AoE) ** - Submission deadline: Wed 15 Feb 2017 - Author notification: Wed 1 Mar 2017 - Camera-ready version: Wed 15 Mar 2017 ** Organizers ** - Coen De Roover, Vrije Universiteit Brussel, Belgium - Anders Møller, Aarhus University, Denmark - Christophe Scholliers, Universiteit Gent, Belgium ** Program Committee (preliminary) ** - Vincent Baltat, Université Paris Diderot, France - Nataliia Bielova, Inria, France - Avid Chaudhuri, Facebook, United States of America - Tobias Distiler, Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany - Jan Martin Jansen, Netherlands Defence Academy, The Netherlands - Frank Piessens, iMinds, Belgium - Rinus Plasmeijer, Radboud University Nijmegen, The Netherlands - Michael Pradel, TU Darmstadt, Germany - Sukyoung Ruy, KAIST, South Korea - Manuel Serrano, Inria, France - Tom Van Cutsem, Nokia Bell Labs, Belgium
[TYPES/announce] LICS 2017: Final Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] FINAL CALL FOR PAPERS Titles & abstracts: 3 Jan 2017 Full papers: 9 Jan 2017 Thirty-Second Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS) 20-23 June 2017, Reykjavik, Iceland http://lics.rwth-aachen.de/lics17/ SCOPE The LICS Symposium is an annual international forum on theoretical and practical topics in computer science that relate to logic, broadly construed. We invite submissions on topics that fit under that rubric. Suggested, but not exclusive, topics of interest include: automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, formal aspects of program analysis, formal methods, foundations of computability, games and logic, higher-order logic, lambda and combinatory calculi, linear logic, logic in artificial intelligence, logic programming, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, probabilistic systems, process calculi, programming language semantics, proof theory, real-time systems, reasoning about security and privacy, rewriting, type systems and type theory, and verification. IMPORTANT DATES Authors are required to submit a paper title and a short abstract of about 100 words in advance of submitting the extended abstract of the paper. The exact deadline time on these dates is given by anywhere on earth (AoE). Titles and Short Abstracts Due: 3 January 2017 Full Papers Due: 9 January 2017 Author Feedback/Rebuttal Period: 28 Feb - 4 March 2017 Author Notification: 21 March 2017 Final Versions Due for Proceedings: 18 April 2017 Deadlines are firm; late submissions will not be considered. All submissions will be electronic via https://www.easychair.org/conferences/?conf=lics2017. SUBMISSION INSTRUCTIONS Every extended abstract must be submitted in the IEEE Proceedings 2-column 10pt format and may be at most 12 pages, including references. LaTeX style files are available on the conference website; please use IEEEtran.cls version V1.8b, released on 26/08/2015. The extended abstract must be in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference and to computer science, all phrased for the non-specialist. Technical development directed to the specialist should follow. References and comparisons with related work must be included. (If necessary, detailed proofs of technical results may be included in a clearly-labeled appendix, to be consulted at the discretion of program committee members.) Submissions not conforming to the above requirements will be rejected without further consideration. Paper selection will be merit-based, with no a priori limit on the number of accepted papers. Papers authored or co-authored by members of the program committee are not allowed. Results must be unpublished and not submitted for publication elsewhere, including the proceedings of other symposia or workshops. The program chair must be informed, in advance of submission, of any closely related work submitted or about to be submitted to a conference or journal. Authors of accepted papers are expected to sign copyright release forms. One author of each accepted paper is expected to present it at the conference. SHORT PRESENTATIONS A session of short presentations, intended for descriptions of student research, works in progress, and other brief communications, is planned. These abstracts will not be published. Dates and guidelines will be posted on the conference website. KLEENE AWARD FOR BEST STUDENT PAPER An award in honour of the late Stephen C. Kleene will be given for the best student paper(s), as judged by the program committee. The 2017 edition of the award is sponsored by the European Association for Theoretical Computer Science (EATCS). SPECIAL ISSUES Full versions of up to three accepted papers, to be selected by the program committee, will be invited for submission to the Journal of the ACM. Additional selected papers will be invited to a special issue of Logical Methods in Computer Science.
[TYPES/announce] Postdoc position in Applied Semantics for Production Architectures
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [please circulate this to any likely candidates - thanks, Peter] Research Associate/Senior Research Associate in Applied Semantics for Production Architectures University of Cambridge Computer Laboratory Research Associate £29,301 - £38,183 or Senior Research Associate £39,324 - 49,772 Fixed-term: until February 28, 2019, when the grant funding the post currently ends. Details: http://www.jobs.cam.ac.uk/job/12397/ Do you want to help build mathematically rigorous foundations for real-world computing, to make it more robust and secure? We have an ongoing project to establish rigorous semantic models for production multiprocessors, to provide a clear basis for programming, software verification, and hardware verification. This involves long-term close collaborations with ARM and IBM, and we have an agreement with ARM to take their internal ISA description, build a mathematical model based on it, integrate it with the concurrency semantics we are developing, and release the whole in a form usable for verification. This will provide the first strongly validated public model for a production multiprocessor architecture. We also have a close collaboration with the CHERI research project, developing processors with hardware-accelerated in-process memory protection and sandboxing, together with an open-source operating system and toolchain based on FreeBSD and Clang/LLVM; formal modelling is at the heart of the CHERI design process. For more details, see some of our previous papers: POPL17 (http://www.cl.cam.ac.uk/~pes20/popl17/mixed-size.pdf), POPL16 ( http://www.cl.cam.ac.uk/~pes20/popl16-armv8/top.pdf), MICRO 2015 ( http://www.cl.cam.ac.uk/~pes20/micro-48-2015.pdf), PLDI11 ( http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/pldi105-sarkar.pdf), CHERI ISA spec (http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.html), CHERI ( https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/), REMS ( http://rems.io). We have a position available to work on: - the development of our Sail metalanguage for ISA description: a language with a lightweight dependent type system, designed to capture ARM, IBM POWER, and CHERI instruction semantics in an engineer-friendly way; - translation from Sail to generate efficient emulators and usable theorem-prover definitions; - mechanised proof about the architecture definitions, e.g. of security properties, relationships between concurrency models, and correctness results for high-level language concurrency compilation; and/or - development of reasoning, symbolic execution, debugging, and/or model-checking tools above the architecture definitions - the initial work should generate many opportunities along these lines. The successful candidate must have a PhD (or equivalent experience), a track-record of publication in relevant areas of Computer Science, good knowledge of English and communication skills, and the expertise and commitment to apply rigorous semantics to real systems. We're looking for people with the skills to make solid models and tools, well-engineered and widely usable. You should have expertise in one or more of: - functional programming (e.g. OCaml) - programming language semantics and type systems - theorem provers, especially Isabelle and/or Coq - symbolic execution - model-checking For senior applicants, e.g. who will be able to contribute substantially to future grant applications, it may be possible to appoint at the Senior Research Associate level. This is part of the broader REMS (Rigorous Engineering for Mainstream Systems) programme grant: a lively collaboration between systems and semantics researchers in Cambridge, Imperial, and Edinburgh to scale up and apply mathematically rigorous semantics to mainstream systems. Informal enquiries should be directed to Peter Sewell ( peter.sew...@cl.cam.ac.uk). To apply online for this vacancy, please click on the 'Apply' button below. This will route you to the University's Web Recruitment System, where you will need to register an account (if you have not already) and log in before completing the online application form. Please ensure you upload your Curriculum Vitae (CV) and a cover letter explaining your potential contribution to the project, as pdf documents. Include the names of 2 or 3 referees at the appropriate point in the online application. Your referees should be prepared to send references within a week of the closing date, if asked by the University. If you upload any additional documents which have not been requested, we will not be able to consider these as part of your application. Please quote reference NR10978 on your application and in any correspondence about this vacancy. The University values diversity and is committed to equality of opportunity. The University has a responsibility to ensure that all employees are eligible to live and work in the UK.
[TYPES/announce] CfP: Workshop SNR affiliated with ETAPS 2017
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR PAPERS SNR 2017 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis April 22, 2017, Uppsala, Sweden Affiliated with ETAPS 2017 http://snr2017.pages.ist.ac.at/ Important Dates === Abstract submission: January 27, 2017 Paper submission: February 3, 2017 Notification: March 10, 2017 Final version: March 24, 2017 Workshop date: April 22, 2017 Scope = Hybrid systems are complex dynamical systems that combine discrete and continuous components. Reachability questions, regarding whether a system can run into a certain subset of its state space, stand at the core of verification and synthesis problems for hybrid systems. There are several successful methods for hybrid systems reachability analysis. Some methods explicitly construct flow-pipes that over-approximate the set of reachable states over time, where efficient computation of such over-approximations requires symbolic representations such as support functions. Other methods based on satisfiability checking technologies, symbolically encode reachability properties as logical formulas, while solving such formulas requires numerically-driven decision procedures. Last but not least, also automated deduction and the usage of theorem provers led to efficient analysis approaches. The goal of this workshop is to bring together researchers working with different reachability analysis techniques and to seek for synergies between the different approaches. The SNR workshop solicits papers broadly in the area of analysis and synthesis of continuous and hybrid systems. The scope of the workshop includes, but is not restricted to, the following topics with application to continuous and hybrid systems: - Reachability analysis - Flow-pipe construction; symbolic state set representations - Logical frameworks for reasoning - Bounded model checking - Automated deduction - Invariant generation - Symbolic execution - Trajectory generation; counterexample computation - Abstraction techniques - Reliable integration - Simulation - Reachability analysis for planning and synthesis - Domain-specific approaches in biology, robotics, etc. - Stochastic/probabilistic hybrid systems Submission Information == The workshop solicits - long research papers (not exceeding 15 pages excluding references), - short research papers (not exceeding 6 pages excluding references) and - work-in-progress papers (not exceeding 6 pages excluding references). Research papers must present original unpublished work which is not submitted elsewhere. In order to foster the exchange of ideas, we also encourage work-in-progress papers, which present recent or on-going work. The papers should be written in English and formatted according to the EPTCS guidelines (http://style.eptcs.org/). Papers can be submitted using the EasyChair system: https://easychair.org/conferences/?conf=snr2017 All submissions will undergo a peer-reviewing process. Accepted research papers will be presented at the workshop and published in the Electronic Proceedings in Theoretical Computer Science (EPTCS, http://www.eptcs.org/). Accepted work-in-progress papers will be presented at the workshop but will not be included in the proceedings. Invited Speakers TBA Workshop Co-Chairs == Erika Abraham (RWTH Aachen University, Germany) Sergiy Bogomolov (Australian National University, Australia) Publicity Chair === Przemyslaw Daca (Institute of Science and Technology Austria, Austria) Program Committee = Matthias Althoff (Technische Universitaet Muenchen, Germany) Stanley Bak (United States Air Force Research Lab, USA) Franck Cassez (Macquarie University, Australia) Xin Chen (University of Colorado at Boulder, USA) Thao Dang (CNRS/VERIMAG, France) Martin Fraenzle (University of Oldenburg, Germany) Goran Frehse (Verimag, France) Antoine Girard (L2S, CNRS, France) Thomas Heinz (Robert Bosch GmbH, Germany) Hui Kong (Institute of Science and Technology Austria, Austria) Oleksandr Letychevskyi (Glushkov Institute of Cybernetics, Ukraine) Nikolaj Nikitchenko (Kyiv National Taras Shevchenko University, Ukraine) Maria Prandini (Politecnico di Milano, Italy) Stefan Ratschan (Academy of Sciences, Czech Republic) Rajarshi Ray (National Institute of Technology Meghalaya, India) Stavros Tripakis (Aalto University, Finland, and UC Berkeley, USA) Vladimir Ulyantsev (ITMO University, Russia) Edmund Widl (Austrian Institute of Technology, Austria) Paolo Zuliani (University of Newcastle, UK)
