ETAPS 2015 Workshops
Sat, 11 April |
Sun, 12 April |
ETAPS Conferences |
Sat, 18 April |
|---|---|---|---|
| GALOP | HotSpot | ||
| GaM | MBT | ||
| QAPL | PLACES | ||
| FMSPLE | DICE | TPDP | |
| FOPARA | FESCA | TTATT | |
| SynCop | VerifyThis | ||
| VPT | WoC | ||
| WPLI | |||
| Pre-SAT-dinner (19:30) | Post-SAT-dinner (19:30) | ||
6th Developments in Implicity Computational ComplExity (DICE)
Sunday, 12 April 2015
http://dice15.computing.dundee.ac.uk
The area of Implicit Computational Complexity (ICC) has grown from several proposals for using logic and formal methods to provide languages for complexity-bounded computation (e.g. PTIME, LOGSPACE computation). Its aim is to study computational complexity without reference to external measuring conditions or particular machine models, but only in terms of language restrictions or logical/computational principles implying complexity properties.
This workshop focuses on ICC methods related to programs. Traditionally, in this approach one relates complexity classes to restrictions on programming paradigms (functional programs, lambda calculi, rewriting systems), such as ramified recurrence, weak polymorphic types, linear logic and linear types, and interpretative measures. This year we also aim at enlarge the scope of DICE to other research areas loosely related to ICC.
The workshop will be open to contributions on various aspects of ICC including (but not exclusively):
- types for controlling complexity
- logical systems for implicit computational complexity
- semantics of complexity-bounded computation
- interpretation-based methods for implicit complexity
- programming languages for complexity-bounded computation
- theoretical foundations of program complexity analysis
- rewriting and termination orderings
- proof complexity and deep inference
- application of implicit complexity to security
- amortized complexity analysis
- linear logic
Organiser: Marco Gaboardi (PC chair) (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Authors are invited to submit an extended abstract of up to 5 pages.
Submission: 30 January 2015
Notification: 16 February 2015
We will have an open call for paper for a journal special issue after the workshop - joint with DICE'14.
12th Formal Engineering approaches to Software Components and Architectures (FESCA)
Sunday, 12 April 2015
http://fesca.ipd.kit.edu/fesca2015
The aim of the FESCA workshop is to bring together junior researchers from formal methods, software engineering, and industry interested in the development and application of formal modelling approaches as well as associated analysis and reasoning techniques with practical benefits for software engineering.
In recent years, the growing importance of functional correctness and the increased relevance of system quality properties (e.g. performance, reliability, security) have stimulated the emergence of analytical and modelling techniques for the design and development of software systems. With the increasing complexity of today's software systems, FESCA aims at addressing two research questions: (1) what role the software architecture can play in systematic addressing of the analytical and modelling challenges, and (2) how formal and semi-formal techniques can be applied effectively to make the issues easier to address automatically, with lower human intervention.
We encourage not only mature research results, submissions presenting innovative ideas and early results of junior researchers are also of a particular interest.
Organisers:
- Bara Buhnova (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Lucia Happe (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Jan Kofron (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Three kinds of submissions are solicited:
* regular papers (up to 15 pages) presenting original and unpublished work related to the workshop topics,
* position papers (up to 10 pages) presenting ideas and directions of interesting ongoing and yet unpublished research related to the workshop topics, and
* tool demonstration papers (up to 8 pages) presenting and highlighting the distinguishing features of a topic-related tool (co-developed by the authors).
The papers should be written in English, follow the EPTCS style, and respect the page limit. Papers are to be submitted via the EasyChair conference system, and need to be registered before submission (authors, title, abstract, keywords). All accepted papers are required to be presented at the workshop by one of the authors. Tool demonstration and position papers are required to state "Tool demonstration paper/Position paper" as a subtitle of the publication.
Final versions of accepted regular and position papers will be published in a volume of the Electronic Proceedings in Theoretical Computer Science (EPTCS). The tool demonstration papers will not appear in the EPTCS proceedings, but will be included in the electronic pre-proceedings (distributed at the workshop) and made available on the workshop website.
Paper registration: 10 December 2014
Submission: 17 December 2014
Notification: 26 January 2015
Camera-ready: 16 February 2015
6th Formal Methods and Analysis in Software Product Line Engineering (FMSPLE)
Saturday, 11 April 2015
Software product line engineering (SPLE) aims to develop a family of systems through systematic, large-scale reuse in order to reduce time-to-market and costs and to increase product quality. Formal methods and analyses offer promising techniques towards realizing these goals. While some analysis approaches (e.g., for feature modelling and variant management) and formal methods (e.g., BDDs, CSPs, SAT solvers, model checkers and formal semantics of variability models) have been applied to SPLE, a considerable potential remains to be exploited. This workshop brings together researchers and practitioners interested in raising the efficiency and the effectiveness of SPLE by applying innovative analysis approaches and formal methods. Participants will be invited to review the state of the art and practice in their respective fields, identify further promising application areas, report practical requirements and constraints from real-world product lines, discuss drawbacks and complements of various approaches, or present new ideas and results.
Topics of interest include, but are not limited to:
- Analysis approaches and formal methods for:
- domain analysis and scoping
- variability modeling
- specification and verification of functional and non-functional properties in SPLE
- safety and security aspects in SPLE
- product line architectures and component-based product line development
- product line implementation, such as type systems, programming languages, formal semantics
- formal verification of product lines and product line artifacts
- correctness-by-construction techniques in SPLE
- automated test case generation and model-based testing in SPLE
- product derivation and application engineering
- product line life-cycle management (e.g., consistency assurance)
- reuse and evolution of SPLs
- Proofs of concept, industrial experiences and empirical evaluations
- Tool presentations
- Vision and position papers on formal methods and analyses applied to SPLE
Organisers: Joanne Atlee, U. Waterloo, Canada (This email address is being protected from spambots. You need JavaScript enabled to view it.) and Stefania Gnesi, ISTI/CNR, Pisa, Italy (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Submission: 30 January 2015
Notification: 27 February 2015
Camera-ready version: 13 March 2015
4th FOundational and Practical Aspects of Resource Analysis (FOPARA)
Saturday, 11 April 2014
The FOPARA workshop will serve as a forum for presenting original research results that are rel- evant to the analysis of resource (e.g. time, space, energy) consumption by computer programs. The workshop aims to bring together the researchers that work on foundational issues with the researchers that focus more on practical results. Therefore, both theoretical and practical con- tributions are encouraged. We also encourage papers that combine theory and practice. The following list of topics is non-exhaustive:
- resource static analysis for embedded or/and critical systems;
- logical and machine-independent characterisations of complexity classes;
- logics closely related to complexity classes;
- type systems for controlling/inferring/checking complexity;
- semantic methods to analyse resources, including quasi-interpretations;
- practical applications of resource analysis;
- complexity analysis by term and graph rewriting.
Organisers: Marko van Eekelen, Radboud University Nijmegen and Open University of the Netherlands (This email address is being protected from spambots. You need JavaScript enabled to view it.)
FOPARA 2015 is a two-phase workshop. All participants are invited to submit a draft paper describing the work to be presented at the workshop. These submissions will be screened by the program committee chair to make sure they are within the scope of FOPARA and will appear in the informal pre-proceedings at the workshop. Submissions appearing in the draft proceedings are not peer-reviewed publications.
After the workshop, authors will be given the opportunity to incorporate the feedback from discussions at the workshop and will be invited to submit a revised full article for the formal review process. These revised submissions will be reviewed by the program committee using prevailing academic standards to select the best articles that will appear in the formal proceedings. The papers selected after the reviewing process will be published as a volume of the Springer LNCS series. The 2013 FOPARA LNCS proceedings volume is still in preparation. The 2009, 2011, 2013 FOPARA proceeding are published as LNCS Volumes 6324, 7177, 8552 (see e.g. DBLP: http://www.informatik.uni-trier.de/ ley/db/conf/fopara/index.html). LNCS is also the expected publication venue for Fopara 2015.
Tentative schedule:
Paper submission: 23 January 2015 (via Easychair)
Notification of acceptance: 16 February 2015
Informal pre-proceedings version due: 2 March 2015
Submission for formal peer-reviewed post proceedings: 29 May 2015
Notification (Paper): 10 July 2015
Camera Ready: 4 September 2015
10th Games for Logic and Programming Languages (GALOP)
11-12 April 2015
Game semantics has emerged as a new and successful paradigm in the field of semantics of logics and programming languages. Game semantics made its breakthrough in computer science in the early 90s, providing an innovative set of methods and techniques for the analysis of logical systems. Subsequently, game-semantic techniques led to the development of the first syntax-independent fully-abstract models for a variety of programming languages, ranging from the purely functional to languages with non-functional features such as control, references or concurrency. There are also emerging connections between game semantics and other semantic theories, notably theories of concurrency such as the pi-calculus, and traditional tree-based semantics of lambda calculi. In addition to semantic analysis, an algorithmic approach to game semantics has recently been developed, with a view to applications in computer assisted verification and program analysis. The workshop provides an opportunity for interaction with other Etaps events and is a major meeting point in the research area of Game Semantics and its applications.
Organiser: Dan Ghica (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Submission: 25 January 2015
Notification: 10 February 2015
1st Graphs as Models (GaM)
11-12 April 2015
GaM seeks to attract and stimulate research on the techniques for graph analysis, inspection and transformation, on a general level rather than in any specific domain. Thus, the concept of a graph (in its many guises) is central; contributions should address scenarios for the use of graphs in a modelling context that potentially transcend specific settings and can be applied across domains. Good, well-known examples of such techniques are model checking and graph transformation; but we welcome contributions on any of the following (non-exhaustive) list of topics:
- The use of graphs in software development, such as synthesis, planning, bug mitigation and repair
- The use of graphs in software analysis, such as verification, testing, static analysis, and simulation
- Graph search optimization techniques such as state space reduction techniques and search heuristics
- Graph algorithms exploiting parallel and distributed architectures, such as clusters, grids and cloud platforms
- Graph algorithms exploiting dedicated hardware, such as graphics processing units and massive storage
- Dedicated algorithms or implementation techniques for graph matching, isomorphism checking, graph distance and other graph-based problems
- Stochastic processes on graphs, including random walks
- Analysis of large graphs, such as large state spaces, social network graphs, large networks, and big (graph) data
- Visual language definition and syntax, such as meta-modelling, grammars and graphical parsing
- Static and dynamic semantics of visual languages, including OCL, graph constraints, simulation and animation
- Model-to-model and model-to-text transformations and their application in model-driven development
- Visual modeling techniques and graph transformations for systems with quality properties like performance, real-time, safety, reliability, and energy consumption
- Case studies and applications
- Tool support for any of the above
Organisers:
- Arend Rensink (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Eduardo Zambon (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Submission: The workshop seeks submissions of three kinds:
- Full papers: We solicit papers of up to 15 pages, in LaTeX format, containing original results. Accepted papers will be published in EPTCS.
- Work-in-progress papers: We solicit papers of up to 15 pages, in LaTeX format, describing ongoing research. Accepted papers will be presented at the workshop and might be selected for publication in EPTCS.
- Informal tool demo proposals: Tool demos are limited to 10 minutes. Proposals will not be reviewed, unless selection turns out to be necessary.
All contributions should be submitted through EasyChair via this link.
Submission: 16 January 2015
Notification: 13 February 2015
Final manuscript: 13 March 2015
3rd Hot Issues in Security Principles and Trust (HotSpot)
Saturday, 18 April 2015
http://www.lucavigano.com/HotSpot2015
This workshop is intended to be a less formal counterpart to the Principles of Security and Trust (POST) conference at ETAPS, and with an emphasis on "hot topics", both of security and of its theoretical foundations and analysis.
Like POST, the themes are
- theory of computer security
- formal specification, analysis and design of security systems
- automated reasoning for security analysis
Submissions about new and emerging topics (for example, those that have not appeared prominently in conferences and workshops until now) are particularly encouraged. Submissions of preliminary, tentative work are also encouraged. There is no page limit, but the length of your submission should be appropriate to its content. There will be no formal proceedings. Inclusion in informal proceedings is optional.
This workshop is organised by IFIP WG 1.7: Theoretical Foundations of Security Analysis and Design.
Organiser: Luca Vigano (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Submission: 5 January 2015
Notification: 6 February 2015
Final versions for informal proceedings (optional): 15 February 2015
10th Model Based Testing (MBT)
Saturday, 18 April 2015
MBT 2015 is devoted to model-based testing of both software and hardware, and new trends in fusion of testing with other model-based verification technologies.
Model-based testing uses models that describe the behavior of the system under consideration to guide test selection and test results evaluation. Model-based testing has gained attention with the popularization of models in software/hardware design and development. Of particular importance are formal models with precise semantics: testing with such models allows measuring the degree of the product's conformance with the model. The intent of this workshop is to bring together researchers and practitioners who use different kinds of models for testing to discuss the state of the art in theory, applications, tools, and industrialization of MBT.
Organisers:
- Alexander K. Petrenko, Institute for System Programming Russian Academy of Sciences, Moscow, Russia (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Holger Schlingloff, Fraunhofer FOKUS and Humboldt-Universität, Berlin, Germany (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Nikolay Pakulin, Institute for System Programming Russian Academy of Sciences, Moscow, Russia (This email address is being protected from spambots. You need JavaScript enabled to view it.)
8th Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES)
Saturday, 18 April 2015
Applications today are built using numerous interacting services; soon off-the-shelf CPUs will host thousands of cores, and sensor networks will be composed from a large number of processing units. Many applications need to make effective use of thousands of computing nodes. At some level of granularity, computation in such systems is inherently concurrent and communication-centred.
To exploit and harness the richness of this computing environment, designers and programmers will utilise a rich variety of programming paradigms, depending on the shape of the data and control flow. Plausible candidates for such paradigms include structured imperative concurrent programming, stream-based programming, concurrent functions with asynchronous message passing, higher-order types for events, and the use of types for communications and data structures (such as session types and linear types), to name but a few. Combinations of these abstractions will be used even in a single application, and the runtime environment needs to ensure seamless execution without relying on differences in available resources such as the number of cores.
The development of effective programming methodologies for the coming computing paradigm demands exploration and understanding of a wide variety of ideas and techniques. This workshop aims to offer a forum where researchers from different fields exchange new ideas on one of the central challenges for programming in the near future, the development of programming methodologies and infrastructures where concurrency and distribution are the norm rather than a marginal concern.
Organisers:
- Simon Gay, University of Glasgow, UK (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Jade Alglave, University College London, UK (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Steering Committee:
- Alastair Beresford, University of Cambridge, UK
- Simon Gay, University of Glasgow, UK
- Alan Mycroft, University of Cambridge, UK
- Vasco Vasconcelos, University of Lisbon, PT
- Nobuko Yoshida, Imperial College London, UK
Submission: Friday 19th December 2014
Notification: Friday 23rd January 2015
Publication: post-proceedings in EPTCS, submissions approx. end May 2015
12th Quantitative Aspects of Programming Languages and Systems (QAPL)
11 - 12 April 2015
Quantitative aspects of computation are important and sometimes essential in characterising the behavior and determining the properties of systems. They are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, security and trust). Such quantities play a central role in defining both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of system properties. The aim of this workshop is to discuss the explicit use of quantitative information such as time and probabilities either directly in the model or as a tool for the analysis of systems. In particular, the workshop focuses on:
- the design of probabilistic, real-time, quantum languages and the definition of semantical models for such languages;
- the discussion of methodologies for the quantitative analysis of systems, for instance probabilistic and timing properties (e.g. security, safety, schedulability) and other quantifiable properties such as reliability (for hardware components), trustworthiness (in information security) and resource usage (e.g., worst-case memory/stack/cache requirements);
- the probabilistic analysis of systems which do not explicitly incorporate quantitative aspects (e.g. performance, reliability and risk analysis);
- applications to safety-critical systems, communication protocols, control systems, asynchronous hardware, adaptive systems, systems biology, and to any other domain involving quantitative issues.
Organisers: Nathalie Bertrand (This email address is being protected from spambots. You need JavaScript enabled to view it.) and Mirco Tribastone (This email address is being protected from spambots. You need JavaScript enabled to view it.)
The proceedings will appear in EPTCS.
Submission: 14 December 2014
Notification: 9 February 2015
2nd Synthesis of Complex Parameters (SynCop)
Saturday, 11 April 2015
http://lipn.univ-paris13.fr/SynCoP2015
SynCoP aims at bringing together researchers working on verification and parameter synthesis for systems with discrete or continuous parameters, in which the parameters influence the behavior of the system in ways that are complex and difficult to predict. Such problems may arise for real-time, hybrid or probabilistic systems in a large variety of application domains. The parameters can be continuous (e.g., timing, probabilities, costs) or discrete (e.g., number of processes). The goal can be to identify suitable parameters to achieve desired behavior, or to verify the behavior for a given range of parameter values.
The scientific subject of the workshop covers (but is not limited to) the following areas:
- parameter synthesis,
- parametric model checking,
- regular model checking,
- robustness analysis,
- parametric logics, decidability and complexity issues,
- formalisms such as parametric timed and hybrid automata, parametric time(d) Petri nets, parametric probabilistic (timed) automata, parametric Markov Decision Processes, networks of identical processes,
- interactions between discrete and continuous parameters,
- applications to major areas of computer science and control engineering.
Organisers: Étenne André (This email address is being protected from spambots. You need JavaScript enabled to view it.) and Goran Frehse (This email address is being protected from spambots. You need JavaScript enabled to view it.)
We welcome submissions of either 12 pages (regular papers) or 4 pages (tool papers). Publication in the OASIcs series (free and open access).
Submission (abstract): 12 January 2015 AoE
Submission (paper): 19 January 2015 AoE
Notification: 27 February 2015
1st Theory and Practice of Differential Privacy (TPDP)
Saturday, 18 April 2015
http://tpdp.computing.dundee.ac.uk
Differential privacy is a promising approach to the privacy-preserving release of data: it offers a strong guaranteed bound on the increase in harm that a user incurs as a result of participating in a differentially private data analysis. Several mechanisms and software tools have been developed to ensure differential privacy for a wide range of data analysis tasks, such as combinatorial optimization, machine learning, answering distributed queries, etc.
Researchers in differential privacy come from several area of computer science as algorithms, programming languages, security, databases, machine learning, as well as from several areas of statistics and data analysis. The workshop is intended to be an occasion for researchers from these different research areas to discuss the recent developments in the theory and practice of differential privacy.
Specific topics of interest for the workshop include (but are not limited to):
- theory of differential privacy,
- verification techniques for differential privacy,
- programming languages for differential privacy,
- models for differential privacy,
- trade-offs between privacy protection and analytic utility,
- differential privacy and surveys,
- relaxations of the differential privacy definition,
- differential privacy vs other privacy notions and methods,
- differential privacy and accuracy,
- practical differential privacy,
- implementations for differential privacy,
- differential privacy and security,
- applications of differential privacy.
Organisers:
- Gilles Barthe, IMDEA Software (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- George Danezis, University College London (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Marco Gaboardi, University of Dundee (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Aaron Roth, University of Pennsylvania (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- C Skinner, London School of Economics (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Authors are invited to submit a short abstract (4-5 pages maximum) of their work.
Submission: 23 January 2015
Notification: 23 February 2015
We will have a journal special issue after the workshop
3rd Trends in Tree Automata and Tree Transducers (TTATT)
Saturday, 18 April 2015
http://www.ulb.ac.be/di/ssd/filiot/TTATT2015
Recently, tree automata and transducers have been combined and applied to various areas in computer science, including rewrite systems, static analysis of software, program transformation, XML document processing, and computational linguistics. This workshop aims to provide an opportunity for researchers from different areas to exchange ideas on the theory and practice of tree automata and tree transducers. The topics of the workshop include, but are not limited to:
- advanced theory of word and tree automata
- advanced theory of word and tree transducers
- their extensions (higher-order/weighted/infinite models)
- relations to TRS, regularity preservation
- application to static analysis and model checking
- application to program transformation
- application to XML document processing
Organiser: Emmanuel Filiot (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Extended abstracts of at most 6 pages are solicited. The work may be in a preliminary stage, or may be a short version of recently published articles or papers submitted elsewhere. Accepted papers will be made available electronically before the workshop. It is planned to publish original papers in formal post-workshop proceedings (TBA soon).
Submission: 9 January 2015
Notification: 10 February 2015
4th VerifyThis
Sunday, 12 April 2015
http://etaps2015.verifythis.org
VerifyThis is the successor of the program verification competitions held at FoVeOOS2011, FM2012 and the Dagstuhl seminar on Evaluating Software Verification Systems: Benchmarks and Competitions.
Its aims are:
- to bring together those interested in formal verification,
- to provide an engaging, hands-on, and fun opportunity for discussion,
- to evaluate the usability of logic-based program verification tools in a controlled experiment that could be easily repeated.
The competition will offer a number of challenges presented in natural language. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will focus on the input-output behavior of programs, yet it is at the discretion of participants to treat only aspects of requirements. Solutions will be judged for correctness, completeness, degree of automation, and elegance.
Organisers:
- Marieke Huisman (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Vladimir Klebanov (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Rosemary Monahan (This email address is being protected from spambots. You need JavaScript enabled to view it.).
3rd Verification and Program Transformation (VPT)
Saturday, 11 April 2015
http://refal.botik.ru/vpt/vpt2015
The aim of the workshop is to bring together researchers working in the fields of Program Verification and Program Transformation. There is a great potential for beneficial interactions between these two fields because:
(i) methods and tools developed in the field of Program Transformation such as partial evaluation, fold/unfold transformations, and supercompilation, have all been applied with success in the field of the verification of infinite state systems and parameterized systems, and
(ii) model checking, abstract interpretation, SAT and SMT solving and automated theorem proving have been used to enhance program transformation techniques. Moreover, the formal certification of program transformation tools, such as refactoring tools and compilers, has recently attracted considerable interest and posed major challenges.
The workshop will provide a forum where researchers from the Verification and Transformation fields may exchange ideas and foster new developments.
Organisers:
- Emanuele De Angelis, University of Chieti-Pescara, Italy (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Alexei Lisitsa, The University of Liverpool, UK (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Andrei P. Nemytykh, Program Systems Institute of RAS, Russia (This email address is being protected from spambots. You need JavaScript enabled to view it.)
- Alberto Pettorossi, Università di Roma Tor Vergata, Italy (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Program Committee:
- Santiago Escobar, University of València, Spain
- Fabio Fioravanti, University of Chieti-Pescara, Italy
- John Gallagher, Roskilde University, Denmark
- Silvio Ghilardi, University of Milano, Italy
- Geoff W. Hamilton, Dublin City University, Republic of Ireland
- Michael Hanus, University of Kiel, Germany
- Andy King, University of Kent, UK
- Michael Leuschel, Heinrich-Heine-Universität Düsseldorf, Germany
- Alexei Lisitsa, The University of Liverpool, UK
- Andrei P. Nemytykh, Program Systems Institute of RAS, Russia (co-chair)
- Alberto Pettorossi, Università di Roma Tor Vergata, Italy (co-chair)
- German Vidal, University of València, Spain
Important Dates:
Abstract submission: 16 January 2015
Paper submission: 6 February 2015
Notification: 3 March 2015
Camera-ready version: 11 March 2015
1st Workshop on Continuations (WoC)
Sunday 12 April 2015
Modern programming languages provide sophisticated control mechanisms, commonly referred to as control operators which are widely used to realize a variety of applications. Since we cannot escape control features, it becomes a challenge to provide them with sound reasoning principles. There is an active research on understanding, representing, and reasoning about elaborated non-local control structures, in particular in declarative programming languages such as functional and logic languages. Ideas and results from this area have impact in many other fields of computer science, like concurrent systems, proof theory, proof mining, web programming and linguistics. The focus of the workshop is on the interplay between syntax and semantics, the question of what a program using control operators means and how it acts.
The study of control operators is a prominent issue in the theory and practice of functional programming languages with a respectable tradition since the 80's which has been rediscovered along the years in several fields of computer science, fostering applications and rising new challenges. In particular the theme of embedding nonfunctional features in purely functional languages seems a good way to reconcile abstraction and methodologically well understood concepts with expressiveness w.r.t. concurrent systems and communication centered programming which are of major interest at present.
A preliminary list of topics includes (but it is not limited to):
- continuations and delimited continuations
- categorical models of continuations
- compositionality and modularity of coninuations
- denotational semantics of control, event structures and causality
- translations, operational semantics and abstract machines
- type systems for control operators and computational lambda calculi
- game semantics of programming languages and of logical proofs
- usage of control operators in proof search and proof mining
- constructive interpretation of non-constructive proofs
Workshop on Programming Languages in Industry (WPLI)
Sunday 12 April 2015
This workshop opens a dialogue between researchers and industry experts in programming languages. Topics include all aspects of developer productivity at scale, from programming language design and implementation to software engineering, including static and dynamic analysis and testing. Industrial impact on software reliability due to modern theorem proving technology is also among the topics.
The goal of this event is to foster collaboration between academia and industry on topics of importance for today's software development practices.
Format: invited talks and a panel.
Organisers:
- Cristiano Calcagno
- Carsten Fuhs (This email address is being protected from spambots. You need JavaScript enabled to view it.)
Workshop Dinners
Sunday 12 and Saturday 18 April
(only for those who registered for the SAT dinner)
The SAT dinners will take place in the function suite of the Dickens Inn. The Dickens Inn is a restyled and reconstructed wooden warehouse building thought to have housed tea or to have been owned by a local brewery. It certainly existed at the turn of the 18th century and may well have been born in the 1700’s.
Address: The Dickens Inn, St Katharine Docks, 2 Marble Quay, London E1W 1UH
Directions: From Queen Mary one should take the District line from Stepney Green Underground Station to Tower Hill Station. From there it is a short 8 minutes walk to the restaurant as shown on the map below:
