[TYPES/announce] Graphical Models for Security (GraMSec 2017) co-located with CSF 2017
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] GraMSec 2017 - call for papers The Fourth International Workshop on Graphical Models for Security Santa Barbara, CA, USA - August 21, 2017 http://gramsec.uni.lu Co-located with CSF 2017 LNCS proceedings confirmed SCOPE Graphical security models provide an intuitive but systematic approach to analyze security weaknesses of systems and to evaluate potential protection measures. Cyber security researchers, as well as security professionals from industry and government, have proposed various graphical security modeling schemes. Such models are used to capture different security facets (digital, physical, and social) and address a range of challenges including vulnerability assessment, risk analysis, defense analysis, automated defensing, secure services composition, policy validation and verification. The objective of the GraMSec workshop is to contribute to the development of well-founded graphical security models, efficient algorithms for their analysis, as well as methodologies for their practical usage. TOPICS The workshop seeks submissions from academia, industry, and government presenting novel research on all theoretical and practical aspects of graphical models for security. The topics of the workshop include, but are not limited to: • Graphical models for threat modeling and analysis • Graphical models for risk analysis and management • Graphical models for requirements analysis and management • Textual and graphical representation for system, organizational, and business security • Visual security modeling and analysis of socio-technical and cyber-physical systems • Graphical security modeling for cyber situational awareness • Graphical models supporting the security by design paradigm • Methods for quantitative and qualitative analysis of graphical security models • Formal semantics and verification of graphical security models • Methods for (semi-)automatic generation of graphical security models • Enhancement and/or optimization of existing graphical security models • Scalable evaluation of graphical security models • Evaluation algorithms for graphical security models • Dynamic update of graphical security models • Game theoretical approaches to graphical security modeling • Attack trees, attack graphs and their variants • Stochastic Petri nets, Markov chains, and Bayesian networks for security • UML-based models and other graphical modeling approaches for security • Software tools for graphical security modeling and analysis • Case studies and experience reports on the use of graphical security modeling paradigm INVITED SPEAKER To be decided. PAPER SUBMISSION We solicit two types of submissions: • Regular papers (up to 15 pages, excluding the bibliography and well-marked appendices) describing original and unpublished work within the scope of the workshop. • Short papers (up to 7 pages, excluding the bibliography and well-marked appendices) describing original and unpublished work in progress. The reviewers are not required to read the appendices, so the papers should be intelligible without them. All submissions must be prepared using the LNCS style: http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0 Each paper will undergo a thorough review process. All accepted (regular and short) papers will be included in the workshop's post-proceedings. The GraMSec 2017 post-proceedings will be published in the Lecture Notes in Computer Science (LNCS) series of Springer. Submissions should be made using the GraMSec 2017 EasyChair web site: https://www.easychair.org/conferences/?conf=gramsec17 IMPORTANT DATES • Submission deadline: Sunday, May 21, 2017 • Acceptance notification: Friday, July 7, 2017 • Workshop: Monday, August 21, 2017 GENERAL CHAIR • Sjouke Mauw, University of Luxembourg, Luxembourg PROGRAM CHAIRS • Peng Liu, Pennsylvania State University, USA • Ketil Stølen, SINTEF Digital and University of Oslo, Norway PC MEMBERS Mathieu Acher, University Rennes 1, Inria, France Massimiliano Albanese, George Mason University, USA Ludovic Apvrille, Télécom ParisTech, France Thomas Bauereiss, DFKI, Germany Kristian Beckers, Technical University of Munich, Germany Giampaolo Bella, University of Catania, Italy Stefano Bistarelli, Università di Perugia, Italy Marc Bouissou, EDF RD, France Frédéric Cuppens, Télécom Bretagne, France Nora Cuppens-Boulahia, Télécom Bretagne, France Binbin Chen, Advanced Digital Sciences Center, Singapore Hervé Debar, Télécom SudParis, France Harley Eades, Augusta University, USA Mathias Ekstedt, KTH - Royal Institute of Technology, Sweden Ulrik Franke, Swedish Institute of Computer Science - SICS, Sweden Frank Fransen, TNO, The Netherlands Olga Gadyatskaya, University of Luxembourg, Luxembourg Paolo Giorgini, University of Trento, Italy Dieter Gollmann, Hamburg University of Technology,
[TYPES/announce] Call for Participation: LogiCS/RiSE Summer School on Logic, AI and Verification [July 3 to 5]
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies in advance should you receive multiple copies of this mail.] -- Call for Participation LogiCS/RiSE Summer School on Logic, AI and Verification July 3 -- 5, 2017, TU Wien, Vienna, Austria http://forsyte.at/laive-summer-school-2017 -- The doctoral college Logical Methods in Computer Science (LogiCS, http://logic-cs.at/phd/) and the Austrian Society for Rigorous Systems Engineering (RiSE, http://arise.or.at/) will host a summer school on Logic, Artificial Intelligence and Verification at TU Wien, Vienna, Austria from July 3 to July 5. The summer school targets master and doctoral students in Computer Science and Mathematics with a strong interest in Logic, Artificial Intelligence and Automated Verification. The event is open to all interested students. The school will feature the following lectures: * Johannes Fuernkranz (TU Darmstadt): Introduction to Machine Learning * Cezary Kaliszyk (University of Innsbruck): Machine Learning in Theorem Proving * Dan Olteanu (University of Oxford): From Joins to Aggregates to Optimization Problems * Diego Calvanese and Marco Montali (Free University of Bolzano-Bozen): Verification of Data-Centric Systems * Matteo Maffei (TU Wien): TBA Register until May 31 to profit from the early registration fee of €70! For more information and registration, see http://forsyte.at/laive-summer-school-2017
[TYPES/announce] 1-2 Ph.D positions on Combining Formal Methods and Machine Learning (U. of Oslo), 9. June 2017
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] __ Up to 2 PH.D POSITIONS in Combining Formal Methods and Machine Learning deadline: 9. June 2017 Dept. of Computer Science, University of Oslo https://www.jobbnorge.no/ledige-stillinger/stilling/137456/phd-research-fellow-combining-formal-methods-and-machine-learning-1-2-positions __ PhD Research Fellow , 1-2 positions * Context A position as PhD Research Fellow in Formal Modeling and Analysis is available at the Department of Informatics, University of Oslo. The fellowship will be for a period of 3 years with no compulsory work and with possibility to extend to 4 years with 25 % compulsory work (teaching responsibilities at the Department or innovation activities in the SIRIUS Center). Starting date is as soon as possible. * Job description The position is funded by SIRIUS (Center for Scalable Data Access in the Oil and Gas Domain), a new Center for Research-Driven Innovation (SFI) at the University of Oslo. It constitutes a long-term research initiative, funded by the Norwegian Research Council involving both academic research teams (UiO, NTNU and Oxford University) as well as industrial partners including operators (Statoil), service companies (Schlumberger and DNV GL) and IT companies (e.g., Computas, Evry, IBM). The center has as its main goal to develop novel technologies to improve our ability to extract and exploit information from large data stores. The position is hosted at the IFI SIRIUS center, the Execution Modeling and Analysis group, where we research systematic model exploration techniques to predict the behavior of software/system executions based on the analysis of models. The main focus of this PhD project will be to develop and study new model-based engineering techniques for context-dependent adaptive systems, exploiting the interplay between systematic model exploration and machine learning techniques. In context-dependent adaptive systems, system behavior depends on some contextual information (e.g., data coming from sensors) and the systems must adapt based on their interactions with the environment. We are interested in investigating techniques that combine formal executable modeling with reinforcement learning algorithms to calibrate models and simulate system behavior where its performance improves over time. Demands on analysis techniques to understand context-dependent adaptive systems are increasing in many industrial areas, such as manufacturing, healthcare, oil, and automotive industries. Through SIRIUS, the PhD student will have the opportunity to collaborate with industry and to apply the developed techniques on real industrial cases. Applicants should submit a statement of research interests or a project outline for the PhD project, but it is expected that the successful candidate will ultimately define their project jointly with their supervisors during the first two months of the fellowship.The application letter should discuss at least one research topic of interest to the candidate, including a brief reflection about the scientific issues involved and the possible choice of theory and method(s). This statement of research purpose should not exceed one page. * Requirements Applicants must hold a Master's degree or equivalent in a relevant field such as computing/informatics/software engineering/machine learning. A solid background in computing science or software engineering is required. Good knowledge on algorithms, formal methods, machine learning, and software development skills and experiences will be considered an advantage when candidates are ranked. Additional formal requirements (excepted documents, procedural questions, etc.) as well as information concerning the university as workplace is available via the link given above.
[TYPES/announce] PPDP 2017: Call For Papers (Abstract 12 May / Paper 19 May)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR PAPERS 19th International Symposium on Principles and Practice of Declarative Programming PPDP 2017 Namur, Belgium, October 9-11, 2017 (co-located with LOPSTR'17) http://complogic.cs.mcgill.ca/ppdp2017 SUBMISSION DEADLINE: 12 May (abstracts) / 19 May (papers) PPDP 2017 is a forum that brings together researchers from the declarative programming communities, including those working in the functional, logic, answer-set, and constraint programming paradigms. The goal is to stimulate research in the use of logical formalisms and methods for analyzing, performing, specifying, and reasoning about computations, including mechanisms for concurrency, security, static analysis, and verification. Submissions are invited on all topics from principles to practice, from foundations to applications. Topics of interest include, but are not limited to ** Language Design: domain-specific languages; interoperability; concurrency, parallelism, and distribution; modules; probabilistic languages; reactive languages; database languages; knowledge representation languages; languages with objects; language extensions for tabulation; metaprogramming. ** Implementations: abstract machines; interpreters; compilation; compile-time and run-time optimization; garbage collection; memory management. ** Foundations: type systems; type classes; dependent types; logical frameworks; monads; resource analysis; cost models; continuations; control; state; effects; semantics. ** Analysis and Transformation: partial evaluation; abstract interpretation; control flow; data flow; information flow; termination analysis; resource analysis; type inference and type checking; verification; validation; debugging; testing. ** Tools and Applications: programming and proof environments; verification tools; case studies in proof assistants or interactive theorem provers; certification; novel applications of declarative programming inside and outside of CS; declarative programming pearls; practical experience reports and industrial application; education. This year the conference will be co-located with the 27th Int'l Symp. on Logic-Based Program Synthesis and Transformation (LOPSTR 2017). IMPORTANT DATES: Abstract Submission:12 May 2017 Paper Submission: 19 May 2017 Paper Rebuttal: 10 July 2017 Notification: 20 July 2017 Final Version: 15 Aug 2017 SUBMISSION CATEGORIES: Submissions can be made in three categories: regular Research Papers, System Descriptions, and Experience Reports. Submissions of Research Papers must present original research which is unpublished and not submitted elsewhere. They must not exceed 12 pages ACM style 2-column (including figures and bibliography). Work that already appeared in unpublished or informally published workshop proceedings may be submitted (please contact the PC chair in case of questions). Submissions of research papers will be judged on originality, significance, correctness, clarity, and readability. Submission of System Descriptions must describe a working system whose description has not been published or submitted elsewhere. They must not exceed 10 pages and should contain a link to a working system. System Descriptions must be marked as such at the time of submission and will be judged on originality, significance, usefulness, clarity, and readability. Submissions of Experience Reports are meant to help create a body of published, refereed, citable evidence where declarative programming such as functional, logic, answer-set, constraint programming, etc., is used in practice. They must not exceed 6 pages. Experience Reports must be marked as such at the time of submission and need not report original research results. They will be judged on significance, usefulness, clarity, and readability. Possible topics for an Experience Report include, but are not limited to: * insights gained from real-world projects using declarative programming * comparison of declarative programming with conventional programming in the context of an industrial project or a university curriculum * curricular issues encountered when using declarative programming in education * real-world constraints that created special challenges for an implementation of a declarative language or for declarative programming in
[TYPES/announce] Learning and Automata workshop: call for participation, early reg deadline 5 May
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR PARTICIPATION Learning and Automata (LearnAut) — LICS 2017 Workshop June 19, Reykjavik (Iceland) Early registration: May 5th (VERY SOON) https://learnaut.wordpress.com/ Grammatical Inference studies machine learning algorithms for classical recursive models of computations like automata and grammars. The expressive power of these models and the complexity of associated computational problems are a major research topic within theoretical computer science. This workshop aims at offering a favorable place for dialogue and at generating discussions between researchers from these two communities. The following papers have been accepted for oral presentation: - Enes Avcu, Chihiro Shibata and Jeffrey Heinz: Subregular Complexity and Deep Learning - Alexander Clark: Strong learning of Probabilistic Context-Free Grammars from Strings - Nathanaël Fijalkow: Bisimulation on Distributions for Markov Decision Processes - Oded Maler and Irini-Eleftheria Mens: On Learning Symbolic Automata over Boolean Alphabets - Ariadna Quattoni, Xavier Carreras and Matthias Gallé. Scalable Spectral Learning of Automata through Maximum Matching - Rick Smetsers: Grammatical Inference as a Satisfiability Modulo Theories Problem In addition, the papers accepted for poster presentation are: - Giovanni Bacci, Giorgio Bacci, Kim Guldstrand Larsen and Radu Mardare: On the Metric-based Approximate Minimization of Markov Chains - Simone Barlocco and Clemens Kupke: Automata Learning: A Modal Logic Perspective - Michael Bukatin and Jon Anthony: Dataflow Matrix Machines as a Model of Computations with Linear Streams - Kaizaburo Chubachi, Diptarama, Ryo Yoshinaka and Ayumi Shinohara: Query Learning of Regular Languages over Large Ordered Alphabets - Joshua Moerman: Learning Product Automata - Tianyu Li, Guillaume Rabusseau and Doina Precup: Neural Network Based Nonlinear Weighted Finite Automata - Alexis Linard, Rick Smetsers, Frits Vaandrager, Umar Waqas, Joost van Pinxten and Sicco Verwer: Learning Pairwise Disjoint Simple Languages from Positive Examples - Xiaoran Liu, Qin Lin, Sicco Verwer and Dmitri Jarnikov: Anomaly Detection in a Digital Video Broadcasting System Using Timed Automata - Guillaume Rabusseau and Joelle Pineau: Multitask Spectral Learning of Weighted Automata - Michal Soucha and Kirill Bogdanov: Efficient Active Learning with Extra States The following top researchers will be invited speakers at LearnAut: - Kim G. Larsen (Aalborg University) - Mehryar Mohri (New York University & Google Research) - Alexandra Silva (University College London) If you have not registered yet to the workshop, and if you are interested by its program, we strongly recommend you to do it as soon as possible (http://www.icetcs.ru.is/lics2017-registration.html). The early registration deadline is on May 5th. Pressures on accommodation possibilities are high, the sooner you book one the better it is (a lot of hotels are unfortunately already full). Looking forward to seeing you at Reykjavik! Borja Balle (Amazon) Leonor Becerra-Bonache (Jean Monnet) Remi Eyraud (Aix-Marseille)
[TYPES/announce] APLAS 2017: Asian Symposium on Programming Languages and Systems, CfP, June 13 deadline
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] * APLAS 2017 Call for Papers 15th Asian Symposium on Programming Languages and Systems Suzhou, China, November 27-29, 2017 https://www-aplas.github.io/ * # Important Dates - Abstract deadline: Tuesday, June 13, 2017 - Paper deadline: Friday, June 16, 2017 - Author response: Wednesday-Friday, July 26-28, 2017 - Author notification: Monday, August 14, 2017 - Camera-ready deadline: Friday, September 1, 2017 - Conference: Monday-Wednesday, November 27-29, 2017 All deadline times are AoE. # About APLAS aims to stimulate programming language research by providing a forum for the presentation of latest results and the exchange of ideas in programming languages and systems. APLAS is based in Asia but is an international forum that serves the worldwide programming languages community. APLAS is sponsored by the Asian Association for Foundation of Software (AAFS), founded by Asian researchers in cooperation with many researchers from Europe and the USA. Past APLAS symposiums were successfully held in Hanoi ('16), Pohang ('15), Singapore ('14), Melbourne ('13), Kyoto ('12), Kenting ('11), Shanghai ('10), Seoul ('09), Bangalore ('08), Singapore ('07), Sydney ('06), Tsukuba ('05), Taipei ('04), and Beijing ('03) after three informal workshops. Proceedings of the past symposiums were published in Springer's LNCS. # Topics The symposium is devoted to foundational and practical issues broadly spanning the areas of programming languages and systems. Papers are solicited on topics such as - semantics, logics, foundational theory - design of languages, type systems, and foundational calculi - domain-specific languages - compilers, interpreters, abstract machines - program derivation, synthesis, and transformation - program analysis, verification, model-checking - logic, constraint, probabilistic, and quantum programming - software security - concurrency and parallelism - tools and environments for programming and implementation Topics are not limited to those discussed in previous symposiums. Papers identifying future directions of programming and those addressing the rapid changes of the underlying computing platforms are especially welcome. Demonstration of systems and tools in the scope of APLAS are welcome to the System and Tool demonstrations category. Authors concerned about the appropriateness of a topic are welcome to consult with program chair prior to submission. # Submission We solicit submissions in two categories: - **Regular research papers** describing original scientific research results, including system development and case studies. Regular research papers *should not exceed 18 pages* in the Springer LNCS format, including bibliography and figures. This category encompasses both theoretical and implementation (also known as system descriptions) papers. In either case, submissions should clearly identify what has been accomplished and why it is significant. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. System descriptions papers should contain a link to a working system and will be judged on originality, usefulness, and design. In case of lack of space, proofs, experimental results, or any information supporting the technical results of the paper could be provided as an appendix or a link to a web page, but reviewers are not obliged to read them. - **System and tool demonstrations** describing a demonstration of a tool or a system that support theory, program construction, reasoning, or program execution in the scope of APLAS. The main purpose of a tool paper is to display a completed, robust and well-documented tool--highlighting the overall functionality of the tool, the interfaces of the tool, interesting examples and applications of the tool, an assessment of the tool's strengths and weaknesses, and a summary of documentation/support available with the tool. Authors of tool demonstration proposals are expected to present a live demonstration of the tool at the conference. It is highly desirable that the tools are available on the web. System and Tool papers should not exceed 8 pages in the Springer LNCS format, including bibliography and figures. They may include an additional appendix of up to 6 extra pages giving the outline, screenshots, examples, etc. to indicate the content of the proposed live demo. Papers should be submitted electronically via the submission web page https://easychair.org/conferences/?conf=aplas2017 using EasyChair. The acceptable format is PDF. Submitted papers must be unpublished and not submitted for publication elsewhere. Papers must be written in English. The proceedings will be published as a volume in Springer's LNCS series. Accepted papers must be
[TYPES/announce] PhD position on Security and Privacy of Location-Based Services at at Chalmers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] PhD position on Security and Privacy of Location-Based Services at Chalmers University of Technology, Sweden Application deadline: May 31, 2017 *Job description* The Department of Computer Science and Engineering at Chalmers University of Technology invites applications for a PhD position in Security and Privacy of Location-Based Services. The PhD student will join a world-leading team of researchers on software security and privacy. Software is often the root cause of vulnerabilities in modern computing systems. By focusing on securing the software, we target principled security mechanisms that provide robust protection against large classes of attacks. The advertised position is on Security and Privacy of Location-Based Services. The position is a part of Wallenberg Autonomous Systems and Software Program (WASP), Sweden's largest individual engineering research program. Location-based services/systems (LBS) see tremendous growth, with application from smartphones to autonomous vehicles and aircraft. This project is on rigorous techniques for security and privacy in LBS, including: -security and privacy foundations of LBS: formal modeling and reasoning for LBS policies; -application-, service-, and system-level mechanisms: enforcing security and privacy policies for LBS by such software-level techniques as informationflow control (IFC), program analysis, and monitoring, and their integration with such hardware-level mechanisms as Isolated Execution Environments (IEE) and infrastructure for secure localization; -cryptographic techniques for LBS: designing and scaling decentralized approaches, such as those enabled by secure multi-party computation. This position will be supervised by Prof. Andrei Sabelfeld http://www.cse.chalmers.se/~andrei/ *Details about employment* PhD student position is limited to five years and normally include 20 per cent departmental work, mostly teaching duties. Salary for the position is as specified in Chalmers' general agreement for PhD student positions. Currently the starting salary is around 30,000SEK a month before tax. The position is intended to start in fall 2017. *Suitable background* Applicants should have a Master's Degree or corresponding degree in Computer Science, Computer Engineering, or in a related discipline. As for all PhD studies, a genuine interest and curiosity in the subject matter and excellent analytical and communication skills, both oral and written, are needed. You may apply even if you have not completed your degree, but expect to do so before the position starts. Knowledge of Swedish is not a prerequisite for applying since English is our working language for research, and we publish internationally. Both Swedish and English are used in undergraduate courses. Half of our researchers and PhD students at the department come from more than 30 different countries. *How to apply* The application should be submitted electronically via the following link: http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job=5052 *The department* The department has about 260 employees from more than 30 countries. The research spans the whole spectrum, from theoretical foundations to applied systems development. There is extensive national and international collaboration with academia and industry all around the world. For more information, see http://www.chalmers.se/en/departments/cse/Pages/default.aspx *Gothenburg, Sweden* Gothenburg is often referred to as the "heart of Scandinavia". "This is Gothenburg" video: https://www.youtube.com/watch?v=QkCgd9YfZ34
[TYPES/announce] PhD and Postdoc positions in Innsbruck
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We invite candidates for multiple PhD student and Postdoc researcher positions to start in 2017 or 2018 in the 5-year project "Strong Modular Proof Assistance: Reasoning across Theories" in the CL group at the University of Innsbruck. The starting date can be negotiated. PhD student positions like Postdoc positions are formal employment in Austria, with a regular salary and benefits. Applications before June 15 will receive a full consideration. A background in proof assistants or machine learning is an advantage. Knowledge of German is not required, the group is international and the language of communication is English. Candidates for a PhD position must hold a MSc in computer science or mathematics and candidates for the postdoctoral position hold a PhD degree in computer science or mathematics. Applications and informal inquiries are welcome, please contact Cezary Kaliszyk (cezary.kalis...@uibk.ac.at). Applications should include a CV and names and contact details of two references. For the Postdoc positions please include a brief research statement. The city of Innsbruck, which hosted the Olympic Winter Games in 1964, 1976 and 2012 (YOG), is superbly located in the beautiful surroundings of the Tyrolean Alps. The combination of the Alpine environment and urban life in this historic town provides a high quality of living. The CL group is one of the leading groups concerned with formalization and certification in the world. More information and links about the project, the group, and the university: http://cl-informatik.uibk.ac.at/cek/smart/ -- Cezary Kaliszyk, University of Innsbruck, http://cl-informatik.uibk.ac.at/cek/
[TYPES/announce] 2nd CFP: Workshop on Type-driven Development (TyDe '17)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR PAPERS 2nd Workshop on Type-Driven Development (TyDe '17) 3 September 2017, Oxford, UK http://tydeworkshop.org/2017 # Goals of the workshop The workshop on Type-Driven Development aims to show how static type information may be used effectively in the development of computer programs. Co-located with ICFP, this workshop brings together leading researchers and practitioners who are using or exploring types as a means of program development. We welcome all contributions, both theoretical and practical, on a range of topics including: - dependently typed programming; - generic programming; - design and implementation of programming languages, exploiting types in novel ways; - exploiting typed data, data dependent data, or type providers; - static and dynamic analyses of typed programs; - tools, IDEs, or testing tools exploiting type information; - pearls, being elegant, instructive examples of types used in the derivation, calculation, or construction of programs. # Invited speaker Andrew Kennedy, Facebook, UK # Program Committee - Nada Amin, EPFL, Switzerland - Ana Bove, Chalmers University of Technology, Sweden - Patricia Johann, Appalachian State University, US - Yukiyoshi Kameyama, University of Tsukuba, Japan - Sam Lindley, The University of Edinburgh, UK (co-chair) - Limin Jia, CMU, US - Assia Mahboubi, INRIA Saclay, France - Liam O’Connor, University of New South Wales, Australia - Nicolas Oury, Jane Street, UK - Jennifer Paykin, University of Pennsylvania, US - Paula Severi, University of Leicester, UK - Tarmo Uustalu, Tallinn University of Technology, Estonia - Jeremy Yallop, University of Cambridge, UK - Brent Yorgey, Hendrix College, US (co-chair) # Proceedings and Copyright We plan to have formal proceedings, published by the ACM. Accepted papers will be included in the ACM Digital Library. Authors must grant ACM publication rights upon acceptance, but may retain copyright if they wish. Authors are encouraged to publish auxiliary material with their paper (source code, test data, and so forth). The proceedings will be freely available for download from the ACM Digital Library from one week before the start of the conference until two weeks after the conference. # Submission details Submissions should fall into one of two categories: - Regular research papers (12 pages) - Extended abstracts (2 pages) The bibliography will not be counted against the page limits for either category. Regular research papers are expected to present novel and interesting research results, and will be included in the formal proceedings. Extended abstracts should report work in progress that the authors would like to present at the workshop. Extended abstracts will be distributed to workshop attendees but will not be published in the formal proceedings. We welcome submissions from PC members (with the exception of the two co-chairs), but these submissions will be held to a higher standard. Submission is handled through HotCRP: https://icfp-tyde17.hotcrp.com/ All submissions should be in portable document format (PDF) and formatted using the ACM SIGPLAN style guidelines: http://www.sigplan.org/Resources/Author/ *Note* that the ACM SIGPLAN style guidelines have changed from previous years! In particular, submissions should use the new ‘acmart’ format and the two-column ‘sigplan’ subformat (not to be confused with the one-column ‘acmlarge’ subformat!). Extended abstracts must be submitted with the label 'Extended abstract' clearly in the title. # Important Dates - Regular paper deadline: Wednesday, 24th May, 2017 - Extended abstract deadline: Wednesday, 7th June, 2017 - Author notification: Wednesday, 28th June, 2017 - Deadline for camera ready version: Saturday, 15th July, 2017 - Workshop: Sunday, 3rd September, 2017 # Travel Support Student attendees with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC program, see its web page: http://www.sigplan.org/PAC/ -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.