- Haskell - Haskell.org

[ANN] Haskell ITA meetup in Bologna, Italy (2016-11-19)
by Francesco Ariis 04 Nov '16

04 Nov '16

Hello -cafe, the Italian Haskell Community (http://haskell-ita.it/) is happy to announce its autumn Haskell meetup! The event is going to be hosted in Bologna, on November 19th. The meeting will be in italian; we are going to form small groups/projects, to see Haskell in action and to share knowledge and opinions on functional programming. Everyone, experienced or not, is welcome, just make sure to have a laptop and a working Haskell environment! For a more detailed description of the event and to register, check: https://www.metooo.io/e/haskell-day-bologna (further information in italian follows) ----- - Dove: Bologna, Giardini Margherita, nella struttura "La Gabbia del Leone" (http://leserre.kilowatt.bo.it/gabbia-del-leone/) presso "Le Serre dei Giardini". - Quando: Sabato 19 Novembre, dalle 10:00 alle 18:00. - Chi: chiunque sia interessato alla programmazione funzionale, indipendentemente dal suo livello di esperienza. - Cosa faremo: lavoreremo in gruppi (2-6 persone circa) su diversi progetti. Ogni persona può scegliere il progetto che vuole, saranno date delle indicazioni sul livelo di conoscienza richiesto per contribuire. Lo scopo è provare a utilizzare Haskell per un progetto concreto, "toccare con mano" il modo che hanno altri di lavorare e di condividere le esperienze nelle numerose pause di gruppo. Lo scopo è puramente didattico, quindi nessuna ansia. - Cosa portare: un computer portatile e un ambiente Haskell configurato. - Come arrivare: dalla Stazione Centrale dei Treni di Bologna, prendere l'autobus 33 (frequenza 15 minuti) e scendere alla fermata "Giardini Margherita" e/o "Porta Santo Stefano" (circa 20 minuti di viaggio). Entrare nei Giardini Margherita, dall'ingresso di Via Castiglione 136 o Via Polischi 9, e recarsi presso "Le Serre dei Giardini", alla struttura "La Gabbia del Leone" (http://leserre.kilowatt.bo.it/gabbia-del-leone/) - Grazie a chi: all'associazione [Kilowatt](http://kilowatt.bo.it/about) che ha messo a disposizione gratuitamente la sala. - Per iscriversi: https://www.metooo.io/e/haskell-day-bologna

1 0

SPIN 2017 - Call for papers
by Klaus Havelund 03 Nov '16

03 Nov '16

SPIN 2017 24th International Symposium on Model Checking of Software Santa Barbara, CA, USA, July 13-14, 2017 http://conf.researchr.org/home/spin-2017 Collocated with ISSTA ------------------------------ The SPIN symposium aims at bringing together researchers and practitioners interested in automated tool-based techniques for the analysis of software as well as models of software, for the purpose of verification and validation. The symposium specifically focuses on concurrent software, but does not exclude analysis of sequential software. Submissions are solicited on theoretical results, novel algorithms, tool development, and empirical evaluation. History: The SPIN symposium originated as a workshop focusing on explicit state model checking, specifically as related to the Spin model checker. However, over the years it has evolved to a broadly scoped symposium for software analysis using any automated techniques, including model checking, automated theorem proving, symbolic execution, etc. SPIN 2017 will be arranged as a ACM SIGSOFT event, collocated with the International Symposium on Software Testing and Analysis (ISSTA 2017): http://conf.researchr.org/home/issta-2017. An overview of the previous SPIN symposia (and early workshops) can be found at: http://spinroot.com/spin/symposia. Topics of interest include, but are not limited to: - Formal verification techniques for automated analysis of software - Formal analysis for modeling languages, such as UML/state charts - Formal specification languages, temporal logic, design-by-contract - Model checking - Automated theorem proving, including SAT and SMT - Verifying compilers - Abstraction and symbolic execution techniques - Static analysis and abstract interpretation - Combination of verification techniques - Modular and compositional verification techniques - Verification of timed and probabilistic systems - Automated testing using advanced analysis techniques - Combination of static and dynamic analyses - Derivation of specifications, test cases, or other useful material via formal analysis - Case studies of interesting systems or with interesting results - Engineering and implementation of software verification and analysis tools - Benchmark and comparative studies for formal verification and analysis tools - Formal methods education and training - Insightful surveys or historical accounts on topics of relevance to the symposium ------------------------------ Submission Guidelines ------------------------------ The contributions to SPIN 2017 will be published as ACM Proceedings, and should be submitted in the ACM Conference Format: https://www.acm.org/publications/proceedings-template. With the exception of survey and history papers, submissions must be original and should not have been published previously or be under consideration for publication while being evaluated for this symposium. We are soliciting two categories of papers: - *Full Research Papers* describing fully developed work and complete results (10 pages); - *Short Papers* presenting tools, technology, experiences with lessons learned, new ideas, work in progress with preliminary results, and novel contributions to formal methods education (4 pages). Papers should be submitted via the EasyChair SPIN 2017 submission website: https://easychair.org/conferences/?conf=spin2017. *Best Paper* awards will be given and announced at the conference. A selection of papers will be invited to a special issue of the *International Journal on Software Tools for Technology Transfer* (STTT). ------------------------------ Important Dates ------------------------------ - Paper Submission: February 10, 2017 (23:59:59 Anywhere on Earth) - Author Notification : April 15, 2017 - Camera-Ready Paper: May 20, 2017 - Symposium : July 13-14, 2017 ------------------------------ Program Chairs ------------------------------ - Hakan Erdogmus, Carnegie Mellon University, USA - Klaus Havelund, NASA/Caltech Jet Propulsion Laboratory, USA ------------------------------ Awards Chair ------------------------------ - Corina Pasareanu, NASA Ames Research Center, USA ------------------------------ Program Committee ------------------------------ - Erika Abraham, RWTH Aachen University, Germany - Christel Baier, Technical University of Dresden, Germany - Tom Ball, Microsoft Research, USA - Ezio Bartocci, Vienna University of Technology, Austria - Dirk Beyer, Ludwig-Maximilians-Universität München (LMU Munich), Germany - Armin Biere, Johannes Kepler University, Austria - Dragan Bosnacki, Eindhoven University of Technology, Netherlands - Zmago Brezocnik, University of Maribor, Slovenia - Sagar Chaki, Software Engineering Institute CMU, USA - Alessandro Cimatti, Fondazione Bruno Kessler, Italy - Lucas Cordeiro, University of Oxford, UK - Patrice Godefroid, Microsoft Research, USA - Susanne Graf, VERIMAG Laboratory, France - Radu Grosu, Vienna University of Technology, Austria - Arie Gurfinkel, University of Waterloo, USA - Gerard Holzmann, NASA/Caltech Jet Propulsion Laboratory, USA - Sarfraz Khurshid, The University of Texas at Austin, USA - Kim Larsen, Aalborg University, Denmark - Stefan Leue, University of Konstanz, Germany - Alice Miller, University of Glasgow, Scotland - Corina Pasareanu, NASA Ames Research Center, USA - Doron Peled, Bar Ilan University, Israel - Neha Rungta, NASA Ames Research Center, USA - Theo Ruys, RUwise, Netherlands - Scott Smolka, Stony Brook University, USA - Scott Stoller, Stony Brook University, United States - Jun Sun, Singapore University of Technology and Design, Singapore - Oksana Tkachuk, NASA Ames Research Center, USA - Stavros Tripakis, University of California, Berkeley, USA - Willem Visser, Stellenbosch University, South Africa - Farn Wang, National Taiwan University, Taiwan - Michael Whalen, University of Minnesota, USA - Anton Wijs, Eindhoven University of Technology, Netherlands

1 0

Strachey 100 conference
by Troy Astarte (PGR) 02 Nov '16

02 Nov '16

Dear all, A final reminder for the conference below. This November marks 100 years since the birth of Christopher Strachey. We are holding a symposium to celebrate his life and research in Oxford on Saturday 19th November. There will also be an exhibition of material from the Strachey archive on Friday 18th November, followed by a banquet dinner at Hertford College on the evening of Friday 18th November. For more information and to register for attendance, please go to http://www.cs.ox.ac.uk/strachey100/. ------------------------------- Christopher Strachey (1916–1975) was a pioneering computer scientist and the founder of the Programming Research Group, now part of the Department of Computer Science at Oxford University. Although Strachey was keenly interested in the practical aspects of computing, it is in the theoretical side that he most indelibly left his mark, notably by creating with Dana Scott the denotational (or as he called it, ‘mathematical’) approach to defining the semantics of programming languages. Strachey also spent time writing complex programs and puzzles for various computers, such as a draughts playing program for the Pilot ACE in 1951. He developed some fundamental concepts of machine-independent operating systems, including an early suggestion for time-sharing, and was a prime mover in the influential CPL programming language. Strachey came from a notable family of intellectuals and artists, perhaps most famous for Christopher’s uncle Lytton, a writer and member of the Bloomsbury group. We will be marking the occasion of 100 years since Christopher Strachey's birth on Saturday 19th November 2016, three days after his birthday, with a symposium of invited speakers. The morning will look back at Strachey’s life and works from a historical and technical perspective, and the afternoon will concern the future of Strachey-inspired theoretical computer science at Oxford University. There will also be a display of related archival material on Friday 18th November for anyone interested, and a banquet dinner at Hertford College on the evening of Friday 18th November. Hope to see many of you there. Best, Troy Astarte

1 0

Call for Workshop Proposals: ICFP 2017
by Lindsey Kuper 01 Nov '16

01 Nov '16

CALL FOR WORKSHOP AND CO-LOCATED EVENT PROPOSALS ICFP 2017 22nd ACM SIGPLAN International Conference on Functional Programming September 3-9, 2017 Oxford, United Kingdom http://conf.researchr.org/home/icfp-2017 The 22nd ACM SIGPLAN International Conference on Functional Programming will be held in Oxford, United Kingdom on September 3-9, 2017. ICFP provides a forum for researchers and developers to hear about the latest work on the design, implementations, principles, and uses of functional programming. Proposals are invited for workshops (and other co-located events, such as tutorials) to be affiliated with ICFP 2017 and sponsored by SIGPLAN. These events should be less formal and more focused than ICFP itself, include sessions that enable interaction among the attendees, and foster the exchange of new ideas. The preference is for one-day events, but other schedules can also be considered. The workshops are scheduled to occur on September 3 (the day before ICFP) and September 7-9 (the three days after ICFP). ---------------------------------------------------------------------- Submission details Deadline for submission: November 19, 2016 Notification of acceptance: December 18, 2016 Prospective organizers of workshops or other co-located events are invited to submit a completed workshop proposal form in plain text format to the ICFP 2017 workshop co-chairs (David Christiansen and Andres Loeh), via email to icfp2017-workshops(a)googlegroups.com by November 19, 2016. (For proposals of co-located events other than workshops, please fill in the workshop proposal form and just leave blank any sections that do not apply.) Please note that this is a firm deadline. Organizers will be notified if their event proposal is accepted by December 18, 2016, and if successful, depending on the event, they will be asked to produce a final report after the event has taken place that is suitable for publication in SIGPLAN Notices. The proposal form is available at: http://www.icfpconference.org/icfp2017-files/icfp17-workshops-form.txt Further information about SIGPLAN sponsorship is available at: http://www.sigplan.org/Resources/Proposals/Sponsored/ ---------------------------------------------------------------------- Selection committee The proposals will be evaluated by a committee comprising the following members of the ICFP 2017 organizing committee, together with the members of the SIGPLAN executive committee. Workshop Co-Chair: David Christiansen (Indiana University) Workshop Co-Chair: Andres Loeh (Well-Typed LLP) General Chair: Jeremy Gibbons (University of Oxford) Program Chair: Mark Jones (Portland State University) ---------------------------------------------------------------------- Further information Any queries should be addressed to the workshop co-chairs (David Christiansen and Andres Loeh), via email to icfp2017-workshops(a)googlegroups.com

1 0

[CFP] RAMiCS 2017
by Damien Pous 27 Oct '16

27 Oct '16

Second Call for Papers ----------------------------------------------------- 16th International Conference on RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE (RAMiCS 2017) May 15-19, 2017 Lyon, France http://ramics-conference.org ----------------------------------------------------- GENERAL INFORMATION: For more than two decades, the RAMiCS conferences series has been the main venue for research on relation algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond. TOPICS: We invite submissions in the general field of algebraic structures relevant to computer science and on applications of such algebras. Topics of the conference include, but are not limited to the following -theory * algebraic structures from semigroups, residuated lattices and semirings to Kleene algebras, relation algebras and quantales * other algebras relevant to the theory of automata, concurrency, formal languages, games, networks, programming languages and social choice * algorithmic, category-theoretic, coalgebraic or proof-theoretic methods for such algebras * their formalisation with automated and interactive theorem provers -applications * tools and techniques for the verification and correctness of sequential and concurrent programs * quantitative and qualitative models for computing systems * logics of programs, e.g., modal, dynamic, interval, temporal or resource logics, logics for games, social choice and distributed systems * design of algorithms, network protocol analysis, optimisation and control INVITED SPEAKERS: * Annabelle McIver (Macquarie University, Sydney) * Jean-Eric Pin (CNRS, IRIF, Paris) * Alexandra Silva (University College, London) IMPORTANT DATES: Abstract Submission: 2016, Nov 25 Paper Submission: 2016, Dec 2 Author Notification: 2017, Feb 3 Camera-ready papers: 2017, Feb 24 RAMiCS 2017: 2017, May 15-19 SUBMISSION INSTRUCTIONS: Submission is via EasyChair at https://www.easychair.org/conferences/?conf=ramics16 All papers will be peer reviewed by at least three referees. The proceedings will be published in an LNCS volume by Springer, ready at the conference. Submissions must be in English, in PDF format and should not exceed 16 pages in LNCS style. Submissions must be unpublished, not under review for publication elsewhere and provide sufficient information to judge their merits. Additional material may be provided in a clearly marked appendix or by a reference to a manuscript on a web site. Experimental data, software or mathematical components for theorem provers must be available in sufficient detail for reviewers. Deviation from these requirements may lead to rejection. Accepted papers must be produced with LaTeX. One author of each accepted paper is expected to present the paper at the conference. Formatting instructions and LNCS style files can be obtained at: http://www.springer.de/comp/lncs/authors.html. COMMITTEES: Conference Chair: Damien Pous, CNRS, France Programme Chairs: Peter Höfner, Data61, Australia Georg Struth, U Sheffield, UK, Programme Committee: Luca Aceto, Reykjavik U, Iceland Rudolf Berghammer, U Kiel, Germany Filippo Bonchi, CNRS, France Jules Desharnais, U Laval, Canada Hitoshi Furusawa, Kagoshima U, Japan Tim Griffin, U Cambridge, UK Walter Guttmann, U Canterbury, New Zealand Robin Hirsch, UCL, UK Peter Höfner, Data61, CSIRO, Australia Marcel Jackson, LaTrobe U, Australia Jean-Baptiste Jeannin, Samsung, USA Peter Jipsen , Chapman U, USA Christian Johansen, U Oslo, Norway Wolfram Kahl, McMaster U, Canada Dexter Kozen, Cornell U, USA Szabolcs Mikulas, Birkbeck U, UK Bernhard Möller, U Augsburg, Germany José N. Oliveira, U Minho, Portugal Damien Pous, CNRS, France Georg Struth, U Sheffield, UK, Pascal Weil, CNRS, France Michael Winter, Brock U, Canada

1 0

CoALP-Ty'16: Call for Participation
by František Farka 27 Oct '16

27 Oct '16

Call for Participation Workshop on Coalgebra, Horn Clause Logic Programming and Types 28-29 November 2016, Edinburgh, UK https://ff32.host.cs.st-andrews.ac.uk/coalpty16/ Abstract submission: 15 October, 2016 Registration deadline: 5 November, 2016 ==================================================== Objectives and scope ------------------- The workshop marks the end of the EPSRC Grant Coalgebraic Logic Programming for Type Inference, by K. Komendantskaya and J. Power and will consist of two parts: Part 1 - Semantics: Lawvere theories and Coalgebra in Logic and Functional Programming Part 2 - Programming languages: Horn Clause Logic for Type Inference in Functional Languages and Beyond We invite all colleagues working in related areas to present and share their results. We envisage a friendly meeting with many stimulating discussions, and therefore welcome presentations of already published research as well as novel results. Authors of original contributions will be invited to submit their papers to EPTCS post-proceedings. We especially encourage early career researchers to present and participate. Venue ----- The workshop will be held at the International Centre for Mathematical Sciences, in Edinburgh city centre, just 2 minutes walk from the Informatics Forum. Registration ------------ To register please fill in https://goo.gl/forms/KAm83p1bcNAxw0ss2 Although the registration is free it is compulsory. Please register by the 5th of November 2016. Programme --------- Monday 28 November 9:10 - 9:20 Registration 9:30 - 9:40 Welcome to CoALP-Ty'16 - Ekaterina Komendantskaya 9:40 - 11:10 Invited talk I - John Power: Logic Programming: Laxness and Saturation 11:10 - 11:30 Coffee break 11:30 - 12:00 Contributed talk - Henning Basold and Ekaterina Komendantskaya: Models of Inductive-Coinductive Logic Programs 12:00 - 13:00 Invited talk II - Steven Ramsay and Luke Ong: Refinement Types and Higher-Order Constrained Horn Clauses 13:00 - 14:00 Lunch 14:00 - 15:00 Invited talk III - Tarmo Uustalu: Comodels and Interaction 15:00 - 15:30 Coffee break 15:30 - 17:00 Contributed talks - František Farka: Proofs by Resolution and Existential Variables - Bashar Igried and Anton Setzer: Defining Trace Semantics for CSP-Agda - Clemens Kupke: Coalgebra and Ontological Rules 18:00 - 20:00 Workshop dinner - Lebanese restaurant Beirut, 24 Nicolson Square Tuesday 29 November 9:30 - 10:30 Invited talk IV - Claudio Russo: Classes for the Masses 10:30 - 11:00 Contributed talk - J. Garrett Morris: Semantical Analysis of Type Classes 11:00 - 11:30 Coffee break 11:30 - 12:30 Invited talk V - Davide Ancona: Abstract Compilation for Type Analysis of Object-Oriented Languages 12:30 - 13:30 Lunch 13:30 - 14:30 Invited talk VI - Ki Yung Ahn: Relational Specification of Type Systems Using Logic Programming 14:30 - 15:15 Discussion Panel - Horn Clause Logic: its Proof Theory, Type Theory and Category Theory — do we have the full picture yet? 15:15 - 15:45 Coffee break 15:45 - 16:45 Contributed talks - Martin Schmidt: Coalgebraic Logic Programming: Implementation and Optimization - Luca Franceschini, Davide Ancona and Ekaterina Komendantskaya: Structural Resolution for Abstract Compilation of Object-Oriented Languages Important dates --------------- Workshop registration: 5 November, 2016 Workshop: 28–29 November, 2016 Programme committee ------------------- Ki Yung Ahn, Nanyang Technological University, Singapore Davide Ancona, University of Genoa, Italy Filippo Bonchi, CNRS, ENS de Lyon, France Iavor Diatchki, Galois, Inc, USA Peng Fu, Heriot-Watt University, Edinburgh, UK Neil Ghani, University of Strathclyde, UK Patricia Johann, Appalachian State University, USA Ekaterina Komendantskaya, Heriot-Watt University, Edinburgh, UK Clemens Kupke, University of Strathclyde, UK J. Garrett Morris, University of Edinburgh, UK Fredrik Nordvall Forsberg, University of Strathclyde, UK John Power, University of Bath, UK Claudio Russo, Microsoft Research Cambridge, UK Martin Schmidt, DHBW Stuttgart and Osnabrück University , Germany Stephan Schulz, DHBW Stuttgart, Germany Aaron Stump, The University of Iowa, USA Niki Vazou, University of California, San Diego, USA Joe Wells, Heriot-Watt University, Edinburgh, UK Fabio Zanasi, Radboud University of Nijmegen, The Netherlands Workshop chairs -------- Ekaterina Komendantskaya, Heriot-Watt University, UK John Power, University of Bath, UK Publicity chair --------------- František Farka, University of Dundee, UK and University of St Andrews, UK -- František Farka

1 0

[ANN] unicode-transforms-0.2.0 pure Haskell unicode normalization
by Harendra Kumar 25 Oct '16

25 Oct '16

Hi, I released unicode-transforms sometime back as bindings to a C library (utf8proc). Since then I have rewritten it completely in Haskell. Haskell data structures are automatically generated from unicode database, so it can be kept up-to-date with the standard unlike the C implementation which was stuck at unicode 5. The implementation comes with a test suite providing 100% code coverage. After a number of algorithmic and implementation efficiency optimizations, I was able to get several times better decompose performance compared to the C implementation. I have not yet got a chance to fully optimize the compose operations but they are still as fast as utf8proc. I would like to thank Antonio Nikishaev for the unicode character database parsing code which I borrowed from the prose library. https://github.com/harendra-kumar/unicode-transforms https://hackage.haskell.org/package/unicode-transforms -harendra

1 0

[ANN] dbmigrations 2.0.0: the "break everything in a good way" update
by Jonathan Daugherty 22 Oct '16

22 Oct '16

Hi, TLDR: this release contains good but BREAKING changes! Read on for details. I'm pleased to announce the release of version 2.0.0 of the "dbmigrations" library for managing relational database schema changes. http://hackage.haskell.org/package/dbmigrations This release includes the creation of three new packages. These are the ones you want to install now, instead of the core library: * http://hackage.haskell.org/package/dbmigrations-postgresql * http://hackage.haskell.org/package/dbmigrations-sqlite * http://hackage.haskell.org/package/dbmigrations-mysql In this release all database-specific functionality was factored out of the core library into the packages listed above. Previously, if you wanted to use dbmigrations you needed to have, say, MySQL C libraries installed even if you didn't want to use dbmigrations on a MySQL database. Needless to say, this created headaches as more backend implementations were added to the library. This means that, as a transition aid, the core package's tool EXITS WITH AN ERROR MESSAGE that suggests you install one of the above backend-specific packages to get a backend-specific version of the dbmigrations tool. The dbmigrations library also includes a backend test suite that all of the backend-specific packages use to ensure consistent behavior across implementations of the dbmigrations interface. This release was made possible by Bastian Krol, who put in a lot of time to move the backend-specific bits of the library into the new packages. This was a much-needed change and I'm thankful for his contribution! -- Jonathan Daugherty

1 0

CFP: Functional Paradigm for High Performance Computing
by John Hughes 19 Oct '16

19 Oct '16

============================================================================ Future Generation Computer Systems (IF=2.430) Special Issue on Functional Paradigm for High Performance Computing in conjunction with the International Conference Lambda Days 2017 http://www.lambdadays.org February 09-10, Kraków, Poland ============================================================================ Dear Sir or Madam, We hereby cordially invite you to submit a paper presenting the results of original research or innovative practical application in the area of Functional Programming for High Performance Computing. The special issue aims to bring together functional programming designers, HPC experts, researchers and application developers from academia and industry to present the latest progress on functional programming paradigm for High Performance Computing and to identify and discuss which possible solutions provided by functional programming are useful for HPC issues. The deadline for submitting your paper to the workshop is November 30th, 2016. For more information and details on the call, please check the link: http://www.journals.elsevier.com/future-generation-computer-systems/call-fo… or the main conference site: www.lambdadays.org<http://www.lambdadays.org> or the PDF CFP online: http://www.lambdadays.org/static/upload/media/1475770130836999pdf_lambda2.p… You can also contact the organizers directly by sending an email to olekb(a)agh.edu.pl<mailto:olekb@agh.edu.pl> With best regards, On behalf of the special section chairs: Aleksander Byrski, AGH University of Science and Technology, Krakow, Poland Katarzyna Rycerz, AGH University of Science and Technology, Krakow, Poland John Hughes, Chalmers University of Technology, Gothenburg, Sweden Kevin Hammond, University of St. Andrews, St. Andrews, Scotland, UK

1 0

2 PhD student positions on securing systems using Haskell
by Alejandro Russo 18 Oct '16

18 Oct '16

[Our apologies if you receive multiple copies of this message] The Software Technology Division of the Computer Science and Engineering Department, Chalmers University of Technology is hiring: - 1 PhD student in Programming Language-based Security http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=4389 - 1 PhD student in Language-based Security using Functional Programming http://www.chalmers.se/en/about-chalmers/vacancies/?rmpage=job&rmjob=4391 PhD student positions are for up to five years of full-time employment; normally, 20% of the time is allocated to departmental work (mainly teaching duties). The salary for the positions is as specified in Chalmers's general agreement for PhD student positions. * Application deadline: 30 November 2016. * Expected starting date: preferably early 2017. ------------------------------------------------------------- 1 PhD student position in Programming Language-based Security ------------------------------------------------------------- Increasingly, security flaws in applications arise due to software errors. Programming Language-based Security is a domain in which we strive to enhance security of software application by looking at properties of programming languages. In the Paragon project, we focus on achieving security of software through the construction and use of a dedicated, statically security-typed programming language. The language Paragon is an extension of Java (implemented in Haskell), adding a type system for information flow control based on an expressive calculus for security policies we have developed. The position focuses on improving and extending the applicability of Paragon to practical programming domains. Of particular interest is the Android operating system, where we envision the construction of a secure, information-flow aware app infrastructure. Research opportunities include: * applying Paragon to case studies in specific software domains, in particular the domain of Android apps. * investigating the interaction of information flow and particular language features such as concurrency or typestate; * applying the principles behind Paragon to other programming languages and paradigms; * proving mathematical properties of type systems; The ideal applicant has a strong working knowledge in programming language technology, including type systems, static analysis, and formal semantics; and also in functional programming, as well as a broad interest in programming languages and paradigms in general. Prior knowledge of software security or Android programming are useful but not essential. To read more about the Paragon project, see the project website (http://www.cse.chalmers.se/research/group/paragon/) We recommend in particular the interactive tutorial (http://cse-212294.cse.chalmers.se/research/paragon/tutorial/) This position will be supervised by Prof. Niklas Broberg and Prof. David Sands. ------------------------------------------------------------------------------ 1 1 PhD student position in Language-based Security using Functional Programming ------------------------------------------------------------------------------ The position focuses on developing techniques to protect confidentiality and integrity of users' data when manipulated by third-party code (i.e., code written by someone else) -- a pressing problem for the web as well as mobile platforms. We expect functional programming to play an important role addressing this challenge. In this direction, researchers at Chalmers have been responsible for developing some of the state-of-the-art tools for protecting users' sensitive data in Haskell programs (e.g., LIO https://hackage.haskell.org/package/lio and MAC https://hackage.haskell.org/package/mac) It is expected that the work carried out by the applicant ranges from establishing new theoretical foundations to deploying prototypes in realistic systems. We are looking for candidates with strong background in programming languages who are also interested in building systems using their ideas. The candidate is expected to pursue one or more of the following topics: * Combining type-systems features and dynamic analysis to secure functional languages, where the main target is Haskell programs. * Leveraging hardware-level security components (e.g, Intel SGX and ARM TrustZones) to provide security in depth, where private data can be protected from the application level down to the low-level physical layers by the use of, for instance, foreign function calls. * Design of secure web frameworks to control the flow of information in an end-to-end fashion, i.e., at the server side as well as in web browsers. We envision the creation of secure web frameworks based on functional reactive programming (FRP). As an introduction to the research area, applicants are recommended to read the article Functional Pearl: Two can keep a secret if one of them uses Haskell (http://www.cse.chalmers.se/~russo/publications_files/pearl-russo.pdf<http://www.cse.chalmers.se/%7Erusso/publications_files/pearl-russo.pdf>). This position will be supervised by Prof. Alejandro Russo (http://www.cse.chalmers.se/~russo/<http://www.cse.chalmers.se/%7Erusso/>)

1 0