November 2015 - Haskell

Haskell-related PhD Studentship at Kent
by Meng Wang 22 Mar '16

22 Mar '16

Dear Haskellers, I am seeking a PhD student on a Haskell-related project: http://www.cs.kent.ac.uk/research/studyingforaphd/phd-wang.html This would be a good opportunity for someone who is interested in applying Haskell ideas to real problems. The funding covers maintenance, EU student fees and research related expenses. But non-EU students are welcome to apply too. For Sep 2015 starting, the application deadline is 17 April 2015. If you are interested, please contact me at m.w.wang(a)kent.ac.uk<mailto:m.w.wang@kent.ac.uk>. Best wishes, Meng — Dr Meng Wang School of Computing University of Kent http://www.cs.kent.ac.uk/people/staff/mw516/

1 1

[ICGT2016] CFP: Int.Conf. Graph Transformation, Vienna, July 2016
by Rachid Echahed 18 Feb '16

18 Feb '16

[Apologies if you receive multiple copies of this CFP] ========================================================================== Call for Papers ICGT 2016 9th International Conference on Graph Transformation www.graph-transformation.org Held as Part of STAF 2016 http://staf2016.conf.tuwien.ac.at/ July 5-6, 2016, Vienna, Austria ========================================================================== Important Dates: Abstract submission: 15 February 2016 Full paper submission: 29 February 2016 Notification of acceptance: 07 April 2016 Final version due: 21 April 2016 Conference: 5-6 July 2016 ========================================================================== Graphs are used almost everywhere when representing or modelling structures and systems, not only in applied and theoretical computer science, but also in, e.g., natural and engineering sciences. Graph transformation and graph grammars are the fundamental modelling paradigms for describing, formalizing, and analyzing graphs that change over time when modelling, e.g., dynamic data structures, systems, or models. The International Conference on Graph Transformation (ICGT) series aims to bring together researchers from different areas in this context and to provide a forum for presenting new results, discussing novel ideas and sharing experience. In order to foster a lively exchange of perspectives on the subject of the conference, the programme committee of the ninth edition of ICGT encourages all kinds of contributions related to graph transformation. Topics of interest include, BUT ARE NOT LIMITED TO the following subjects: - General models of graph transformation (e.g., high-level, adhesive, node, edge, and hyperedge replacement systems) - Analysis and verification of graph transformation systems - Graph theoretical properties of graph languages - Automata on graphs and parsing of graph languages - Logical aspects of graph transformation - Computational models based on graph transformation - Structuring and modularization concepts for graph transformation systems - Hierarchical graphs and decompositions of graphs - Parallel, concurrent, and distributed graph transformation - Modelling and analysis of dynamic data structures - Term graph rewriting - Graph transformation and Petri nets - Ontologies and ontology evolution - Graph databases - Modelling and realizing software architectures, refactoring, evolution, workflows, business processes, access control, security policies, service-oriented applications, semantic web, ... - Natural language processing, natural computing, bioinformatics, quantum computing, ubiquitous computing, visual computing, image generation, natural and engineering sciences, ... - Model-driven development and model transformation based on graph transformation - Model checking, program verification, simulation and animation - Syntax, semantics and implementation of programming languages, domain-specific languages, and visual languages - Graph transformation languages and tool support - Efficient algorithms (pattern matching, graph traversal etc.) The 9th International Conference on Graph Transformation (ICGT 2016) will be held in Vienna, Austria, as a STAF event (http://staf2016.conf.tuwien.ac.at/) The conference takes place under the auspices of EATCS (http://www.eatcs.org/) EASST (http://www.easst.org/) and IFIP (http://www.ifip.org/) WG 1.3. Program Committee ----------------- Rachid Echahed (Co-Chair, CNRS and University of Grenoble Alpes, France) Mark Minas (Co-Chair, Universität der Bundeswehr München, Germany) Gábor Bergmann (Budapest University of Technology and Economics, Hungary) Paolo Bottoni (Sapienza Univ. di Roma, Italy) Andrea Corradini (Università di Pisa, Italy) Juan de Lara (Universidad Autonoma de Madrid, Spain) Frank Drewes (Umeå University, Sweden) Claudia Ermel (Technische Universität Berlin, Germany) Holger Giese (Hasso Plattner Institute, University of Potsdam, Germany) Annegret Habel (Universität Oldenburg, Germany) Reiko Heckel (University of Leicester, UK) Berthold Hoffmann (Universität Bremen, Germany) Dirk Janssens (Universiteit Antwerpen, Belgium) Barbara König (University of Duisburg-Essen, Germany) Christian Krause (SAP Innovation Centre Potsdam, Germany) Sabine Kuske (Universität Bremen, Germany) Leen Lambers (Hasso Plattner Institute, University of Potsdam, Germany) Yngve Lamo (Bergen University College, Norway) Tihamér Levendovszky (Vanderbilt University, USA) Mohamed Mosbah (LaBRI , Université de Bordeaux, France) Fernando Orejas (Technical University of Catalonia, Spain) Francesco Parisi-Presicce (Sapienza Univ. di Roma, Italy) Detlef Plump (University of York, UK) Arend Rensink (University of Twente, The Netherlands) Leila Ribeiro (Universidade Federal do Rio Grande do Sul, Brazil) Andy Schürr (Technische Universität Darmstadt, Germany) Martin Strecker (Université de Toulouse, France) Gabriele Taentzer (Philipps-Universität Marburg, Germany) Matthias Tichy (University of Ulm, Germany) Pieter Van Gorp (Eindhoven University of Technology, The Netherlands) Hans Vangheluwe (Universiteit Antwerpen, Belgium) Bernhard Westfechtel (University of Bayreuth, Germany) Albert Zündorf (Kassel University, Germany) Paper Submission ---------------- Papers are solicited in three categories: * Research papers (limited to 16 pages in Springer LNCS format) describe innovative contributions and are evaluated with respect to their originality, significance, and technical soundness. Additional material intended for reviewers but not for publication in the final version may be included in a clearly marked appendix. * Case studies (limited to 12 pages in Springer LNCS format) describe applications of graph transformations in any application domain. * Tool presentation papers (limited to 12 pages in Springer LNCS format) demonstrate the main features and functionality of graph-based tools. A tool presentation paper may have an appendix with a detailed demo description (up to 5 pages), which will be reviewed but not included in the proceedings. Papers can be submitted at http://www.easychair.org/conferences/?conf=icgt2016. Submitted papers must use Springer's LNCS format (http://www.springer.com/lncs) Simultaneous submission to other conferences with proceedings or submission of material that has already been published elsewhere is not allowed. The page limits are strict and include references. Proceedings will be published by Springer in the Lecture Notes in Computer Science (http://www.springer.com/lncs) series. Important Dates --------------- Abstract submission: 15 February 2016 Full paper submission: 29 February 2016 Notification of acceptance: 07 April 2016 Final version due: 21 April 2016 Conference: 5-6 July 2016 Further Information ------------------- Web page: http://www.graph-transformation.org https://sites.google.com/site/icgt2016/ Contact: icgt2016(a)gmail.com

1 1

ANN: HaskRel; Employing GHC as a DBMS with support for the relational algebra
by Thor Michael Støre 31 Dec '15

31 Dec '15

Hello, After much scratching of my head over intricate parts of this "Haskell" thing I'm happy to announce that I've finally released my first effort in it: HaskRel. Overview -------- Because I've spent quite a bit of time on database prompts I thought it would be a fun exercise to see how much GHC can be made to operate like a DBMS, and how much of the relational model of database management (as defined by Chris Date et al. today) I'm able to make it accommodate. I'm pleased to register that the relational algebra, base variables and assignment works as one would expect at a database prompt. It does not qualify as an actual RDBMS (unsurprisingly), since it doesn't implement many other things that are required for it to be a proper RDBMS, either because I haven't gotten around to it or they cannot be implemented in Haskell. I've put the source up on GitHub and published it on Hackage: Hackage: http://hackage.haskell.org/package/HaskRel GitHub: https://github.com/thormick/HaskRel/tree/master/HaskRel HaskRel employs a Data.Set of Data.HList.Record as a relation type, for which it defines "Relation" as a synonym. It supports base variables (files) of this type, and implements the functions of the relational algebra such that they can be expressed upon both constants or literal values, upon variables, and upon expressions on variables. Example ------- The following is a minimal definition of a database with a single relation variable, "sp": module MiniDB where import Data.HList.CommonMain import Database.HaskRel.RDBMS sp :: Relvar '[Attr "sno" String, Attr "pno" String, Attr "qty" Integer] sp = Relvar "SP.rv" "Attr" has been defined as a synonym for "Data.Tagged.Tagged", because that is employed to represent what are known as attributes in relational theory. Loading this in GHCi we can first create a relation constant, do some relational assignment, and print the results (pardon the long lines): *MiniDB> let s = ( relation' [ ( "S1", "Smith", 20, "London" ), ( "S2", "Jones", 10, "Paris" ), ( "S3", "Blake", 30, "Paris" ) ] :: Relation '[Attr "sno" String, Attr "sName" String, Attr "status" Integer, Attr "city" String] ) *MiniDB> pt s ┌───────────────┬─────────────────┬───────────────────┬────────────────┐ │ sno :: String │ sName :: String │ status :: Integer │ city :: String │ ╞═══════════════╪═════════════════╪═══════════════════╪════════════════╡ │ S1 │ Smith │ 20 │ London │ │ S2 │ Jones │ 10 │ Paris │ │ S3 │ Blake │ 30 │ Paris │ └───────────────┴─────────────────┴───────────────────┴────────────────┘ *MiniDB> sp `assign` ( relation' [ ("S1", "P1", 300), ("S1", "P3", 400), ("S1", "P5", 100), ("S2", "P1", 300), ("S3", "P2", 200) ] :: Relation '[Attr "sno" String, Attr "pno" String, Attr "qty" Integer] ) Value assigned to ./SP.rv *MiniDB> pt sp ┌───────────────┬───────────────┬────────────────┐ │ sno :: String │ pno :: String │ qty :: Integer │ ╞═══════════════╪═══════════════╪════════════════╡ │ S1 │ P1 │ 300 │ │ S1 │ P3 │ 400 │ │ S1 │ P5 │ 100 │ │ S2 │ P1 │ 300 │ │ S3 │ P2 │ 200 │ └───────────────┴───────────────┴────────────────┘ (Mind that correct display of the Unicode table drawing characters depends on using the right fixed-width font.) Fundamental operations of the relational algebra can of course be performed on them: *MiniDB> p $ s `naturalJoin` sp ┌─────┬───────┬────────┬────────┬─────┬─────┐ │ sno │ sName │ status │ city │ pno │ qty │ ╞═════╪═══════╪════════╪════════╪═════╪═════╡ │ S1 │ Smith │ 20 │ London │ P1 │ 300 │ │ S1 │ Smith │ 20 │ London │ P3 │ 400 │ │ S1 │ Smith │ 20 │ London │ P5 │ 100 │ │ S2 │ Jones │ 10 │ Paris │ P1 │ 300 │ │ S3 │ Blake │ 30 │ Paris │ P2 │ 200 │ └─────┴───────┴────────┴────────┴─────┴─────┘ A proper relational database management system (which, again, this isn't, for several other reasons) must support type inference for relational expressions (see The Third Manifesto, relational model prescription 18). Fortunately, that is of course no problem for GHC with the right extensions: *MiniDB> :t s s :: Relation '[Attr "sno" String, Attr "sName" String, Attr "status" Integer, Attr "city" String] *MiniDB> :t sp sp :: Relvar '[Attr "sno" String, Attr "pno" String, Attr "qty" Integer] *MiniDB> :t s `naturalJoin` sp s `naturalJoin` sp :: IO (containers-0.5.6.2:Data.Set.Base.Set (RTuple '[Tagged "sno" String, Tagged "sName" String, Tagged "status" Integer, Tagged "city" String, Tagged "pno" [Char], Tagged "qty" Integer])) DML is also supported, of course: *MiniDB> insert sp ( relation' [ ("S1", "P2", 200), ("S1", "P3", 400), ("S1", "P4", 200) ] :: Relation '[Attr "sno" String, Attr "pno" String, Attr "qty" Integer] ) Inserted 2 of 3 tuples into ./SP.rv Concise expression of "update" require a set of language extensions (this in addition to DataKinds, which this module enables by default since it is quite ubiquitous in this endeavor): *MiniDB> :set -XQuasiQuotes -XKindSignatures -XViewPatterns *MiniDB> :{ *MiniDB| update sp (\[pun|pno qty|] -> ( pno == "P2" || pno == "P3" || pno == "P4" ) && qty < 300 ) *MiniDB| (\[pun|qty|] -> case qty + 50 of qty -> [pun|qty|]) *MiniDB| :} Updated 3 of 7 tuples in ./SP.rv *MiniDB> pt$ sp `restrict` \[pun|pno|] -> ( pno == "P2" || pno == "P3" || pno == "P4" ) ┌───────────────┬───────────────┬────────────────┐ │ sno :: String │ pno :: String │ qty :: Integer │ ╞═══════════════╪═══════════════╪════════════════╡ │ S1 │ P2 │ 250 │ │ S1 │ P3 │ 400 │ │ S1 │ P4 │ 250 │ │ S3 │ P2 │ 250 │ └───────────────┴───────────────┴────────────────┘ And of course delete-by-predicate: *MiniDB> count sp 7 *MiniDB> deleteP sp (\[pun|pno|] -> pno == "P3") Deleted 1 tuples from SP.rv *MiniDB> count sp 6 For an overview of the functions of the relational algebra and relational assignment defined by HaskRel see: http://hackage.haskell.org/package/HaskRel/docs/Database-HaskRel-Relational… Summary ------- This is a personal, spare-time project, the motivations for which have been to learn Haskell, and see how much of the relational model Haskell/GHC can accommodate, or how much like an RDBMS GHC can operate. Making this practically usable has not been part of the scope. Ascertaining that Haskell/GHC accommodates the relational algebra, relational base variables and operations thereupon in such a straight forward manner, was quite nice. It was particularly fun to see how this allowed examples of expressions in Tutorial D from Chris Date's "SQL and Relational Theory, 2nd. ed" to be expressed in Haskell in a manner quite verbatim to the originals (see https://github.com/thormick/HaskRel/blob/master/HaskRel/examples/SuppliersP… and chapters 6 and 7 of said book). It was also interesting to see trivial querying and DML operations on GHCi operate in a manner similar to what one would expect in a DBMS. Even if this isn't of practical use I still hope it is of some interest, or at least that it can enable Haskell as a demonstrator of some parts of the relational model for database management. Thanks, Thor Michael Støre

3 2

First Call for Papers: Special Issue of the SCP on Automated Verification of Critical Systems
by Lin, Yuhui 30 Nov '15

30 Nov '15

Science of Computer Programming Special Issue on Automated Verification of Critical Systems First Call for Papers Guest editors: Gudmund Grov & Andrew Ireland Submission deadline: 20 May 2016 Notification: 31 August 2016 This special issue is devoted to the 15th international workshop on Automated Verification of Critical Systems (AVoCS 2015), hosted in September 2015 by Heriot-Watt University in Edinburgh (UK): https://sites.google.com/site/avocs15/ The aim of AVoCS is to contribute to the interaction and exchange of ideas among members of the international research community on tools and techniques for the verification of critical systems. These topics are to be interpreted broadly and inclusively. It covers all aspects of automated verification, and typical (but not exclusive) topics of interest are: - Model Checking - Automatic and Interactive Theorem Proving - SAT, SMT or Constraint Solving for Verification - Abstract Interpretation - Specification and Refinement - Requirements Capture and Analysis - Verification of Software and Hardware - Specification and Verification of Fault Tolerance and Resilience - Probabilistic and Real-Time Systems - Dependable Systems - Verified System Development - Industrial Applications Submission to this special issue is open. We expect original articles (typically 20-30 pages) that present high-quality contributions, have not been previously published in an archival venue and that must not be simultaneously submitted for publication elsewhere. Submissions must be written in English and comply with SCP's author guidelines http://www.elsevier.com/wps/find/journaldescription.cws_home/505623/authori… Submission is over the SCP website: http://ees.elsevier.com/scico/default.asp which you will have to register for if you do not have an account. When submitting your paper please choose the article type "Special issue: AVoCS 2015". Please send any queries you may have to Gudmund Grov (G.Grov(a)hw.ac.uk) ----- We invite research leaders and ambitious early career researchers to join us in leading and driving research in key inter-disciplinary themes. Please see www.hw.ac.uk/researchleaders for further information and how to apply. Heriot-Watt University is a Scottish charity registered under charity number SC000278.

1 0

JFP Issue on Dependently typed programming: second call for papers
by Wouter Swierstra 30 Nov '15

30 Nov '15

----------------------------------------------------------------------------- CALL FOR PAPERS JFP Special Issue on Dependently typed Programming Submission Deadline: January 11th, 2016 Expected Publication Date: Late 2016 ----------------------------------------------------------------------------- # Scope Over the last years there has been sustained interest in functional programming languages with dependent types. The foundations of dependently typed programming can be traced back to work by Martin-Löf from the 1970s. More recently, the increased popularity of systems such as Agda, Coq, Idris, and many others, reflects the growing momentum in this research area. The Journal of Functional Programming will devote a special issue to programming with dependent types. The purpose of this special issue is to present the state of the art in dependently typed programming languages and their applications. We would like to invite authors to submit papers on all topics relating to programming languages with dependent types, including theory, applications, and language design and implementation. We encourage the submission of consolidated, condensed and extended work based on prior conference and workshop publications. # Submission Details Manuscripts should be submitted in PDF format through the Journal of Functional Programming's website: https://mc.manuscriptcentral.com/cup/jfp_submit Further submission and formatting details can be found on the JFP website. Please submit your paper under the 'DTP Special issue' category. Guest Editors ------------------------------------------------------------------------------ Peter Dybjerpeterd(a)chalmers.se Chalmers University of Technology Sweden Wouter Swierstraw.s.swierstra(a)uu.nl Universiteit Utrecht The Netherlands ------------------------------------------------------------------------------

1 0

Research Fellows in Computing at Oxford Brookes University
by Clare Martin 27 Nov '15

27 Nov '15

Research Fellows in Computing Starting Salary: £29,847, rising annually to £32,600 (pro rata) Full Time, Fixed Term - Researcher The posts (amounting to 1.5FTE) are available from 1st February 2016, for 3 years. The time commitment for each post is negotiable, between 0.5 FTE and full-time. If part-time, there will also be the opportunity of additional employment as a departmental teaching assistant.The Research Fellow will join an interdisciplinary team working on the EU PEPPER project: Patient Empowerment through Predictive PERsonalised decision support. PEPPER is a 36-month research and innovation programme funded by European Union’s Horizon 2020 with total budget approaching €4 million. The project is led by Clare Martin. The purpose of the PEPPER project is to develop a personalised decision support system for type 1 diabetes management that will make predictions based on real-time data in order to empower individuals to improve self-management. The research will also examine the extent to which human behavioural factors and usability issues have previously hindered the wider adoption of personal guidance systems for chronic disease self-management. The UK partners in the project are Imperial College London and Cellnovo Ltd; the remaining partners are based in Spain and Romania. For more information see http://www.jobs.ac.uk/job/AMN228/research-fellow-in-computing/ Please feel free to contact me if you have any questions. Clare -- Clare Martin Principal Lecturer for Student Experience Faculty of Technology, Design and Environment, Oxford Brookes University, Wheatley Campus, Wheatley, Oxford OX33 1HX t: +44 (0) 1865 484543 e: cemartin(a)brookes.ac.uk

1 0

PhD studentships at the Functional Programming Lab in Nottingham
by Henrik Nilsson 27 Nov '15

27 Nov '15

Dear Haskellers, The School of Computer Science in Nottingham is advertising 10 fully- funded PhD studentships. Applicants in the area of the Functional Programming lab (fp.cs.nott.ac.uk) are highly encouraged! If you are interested in applying, please contact a potential supervisor in the FP lab prior to submitting your application: Thorsten Altenkirch - constructive logic, proof assistants, homotopy type theory, category theory, lambda calculus. Venanzio Capretta - type theory, mathematical logic, corecursive structures, proof assistants, dependently-typed programming. Graham Hutton - program construction and verification, category theory, recursion operators, coinductive types. Henrik Nilsson - functional reactive programming, modelling and simulation, probabilistic languages, and design and implementation of declarative domain-specific languages in general. See below for full details. All the best, /Henrik +-----------------------------------------------------------+ 10 Fully-Funded PhD Studentships School of Computer Science University of Nottingham, UK http://nottingham.ac.uk/jobs/currentvacancies/ref/SCI1498 Applications are invited for up to ten fully-funded PhD studentships in the School of Computer Science at the University of Nottingham, starting on 1st October 2016. The topics for the studentships are open, but should relate to the interests of one of the School’s research groups: Agents Lab; Automated Scheduling, Optimisation and Planning; Computer Vision Lab; Functional Programming Lab; Intelligent Modelling and Analysis; Mixed Reality Lab and in the area of Data Science. The studentships are for three years and include a stipend of £14,507 per year and tuition fees, and are available to students of any nationality. Applicants are normally expected to have a first-class Masters or Bachelors degree in Computer Science or a related discipline, and must obtain the support of a potential supervisor in the School prior to submitting their application. Initial contact with supervisors should be made at least two weeks prior to the closing date for applications. Informal enquiries may be addressed to Christine.Fletcher(a)nottingham.ac.uk. To apply, please submit the following items by email to the above address: (1) a brief covering letter that describes your reasons for wishing to pursue a PhD, your proposed research area and topic, and the name of a potential supervisor; (2) a copy of your CV, including your actual or expected degree class(es), and results of all University examinations; (3) an example of your technical writing, such as a project report or dissertation; (4) contact details for two academic referees. Closing date for applications: 19th February 2016 +-----------------------------------------------------------+ This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

1 0

CFP: EOOLT 2016
by Henrik Nilsson 27 Nov '15

27 Nov '15

Dear Haskellers, I would like to draw your attention to EOOLT 2016: the 7th International Workshop on Equation-Based Object-Oriented Languages and Tools. EOOLT may be of interest to anyone interested in applying functional/declarative programming to modelling and simulation of physical systems, for example through the route of embedded domain-specific languages. It is particularly relevant for people with an interest in Functional Reactive Programming (FRP) or the synchronous dataflow paradigm more generally. EOOLT 2016 will take place in Milano, Italy, on 18 April 2016, and the submission deadline is 25 January. The call for papers can be found here: http://eoolt.org/2016/index.php?id=cfp and general information about EOOLT 2016 here: http://eoolt.org/2016/ All the best, /Henrik -- Henrik Nilsson School of Computer Science The University of Nottingham nhn(a)cs.nott.ac.uk This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. This message has been checked for viruses but the contents of an attachment may still contain software viruses which could damage your computer system, you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.

1 0

NFM 2016 - first call for papers
by Klaus Havelund 26 Nov '15

26 Nov '15

NFM 2016 - Call For Papers The 8th NASA Formal Methods Symposium ------------------------------------- http://crisys.cs.umn.edu/nfm2016 June 07 - June 09 2016 McNamara Alumni Center University of Minnesota 200 Oak Street S.E., Minneapolis, MN 55455 Theme of the Symposium ---------------------- The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and the aerospace industry requires advanced techniques that address their specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and the industry, with the goal of identifying challenges and providing solutions towards achieving assurance for such critical systems. New developments and emerging applications like autonomous on-board software for Unmanned Aerial Systems (UAS), UAS Traffic Management (UTM), advanced separation assurance algorithms for aircraft, and the need for system-wide fault detection, diagnosis, and prognostics provide new challenges for system specification, development, and verification approaches. Similar challenges need to be addressed during development and deployment of on-board software for spacecraft ranging from small and inexpensive CubeSat systems to manned spacecraft like Orion, as well as for ground systems. The focus of the symposium will be on formal techniques and other approaches for software assurance, their theory, current capabilities and limitations, as well as their potential application to aerospace, robotics, and other NASA-relevant safety-critical systems during all stages of the software life-cycle. Topics of interest include but are not limited to ------------------------------------------------- * Model checking * Theorem proving * SAT and SMT solving * Symbolic execution * Static analysis * Model-based development * Runtime verification * Software and system testing * Safety assurance * Fault tolerance * Compositional verification * Security and intrusion detection * Design for verification and correct-by-design techniques * Techniques for scaling formal methods * Applications of formal methods in the development of: * autonomous systems * safety-critical artificial intelligence systems * cyber-physical, embedded, and hybrid systems * fault-detection, diagnostics, and prognostics systems * Use of formal methods in: * assurance cases * human-machine interaction analysis * requirements generation, specification, and validation * automated testing and verification Important Dates --------------- - Paper Submission: 2/19/2016 - Paper Notifications: 4/8/2016 - Camera-ready Papers: 4/27/2016 - Symposium: 6/7 - 6/9/2016 Location -------- The symposium will take place at McNamara Alumni Center, University of Minnesota. Registration is required but is free of charge. Submission Details ------------------ There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (maximum 15 pages) 2. Short papers on tools, experience reports, or work in progress with preliminary results (maximum 6 pages) All papers must be in English and describe original work that has not been published or submitted elsewhere. All submissions will be fully reviewed by at least three members of the Program Committee. Papers will appear in a volume of Springer's Lecture Notes in Computer Science (LNCS), and must use LNCS style formatting. Papers must be submitted in PDF format at the EasyChair submission site: https://easychair.org/conferences/?conf=nfm2016 Authors of selected best papers may be invited to submit an extended version to a special issue of the Journal of Automated Reasoning (Springer). Organizing Committee -------------------- - Michael Lowry, NASA Ames Research Center, USA (NASA Liaison) - Johann Schumann, SGT, Inc./NASA Ames Research Center, USA (General Chair) - Oksana Tkachuk, SGT, Inc./NASA Ames Research Center, USA (PC Chair) - Sanjai Rayadurgam, University of Minnesota, USA (PC Chair) - Mike Whalen, University of Minnesota, USA (Financial Chair) - Mats Heimdahl, University of Minnesota, USA (Local Arrangements Chair) Program Committee ----------------- - Julia Badger, NASA Johnson Space Center, USA - Clark Barrett, New York University, USA - Saddek Bensalem, Verimag and University Joseph Fourier, France - Dirk Beyer, University of Passau, Germany - Borzoo Bonakdarpour, McMaster University, Canada - Alessandro Cimatti, FBK, Italy - Darren Cofer, Rockwell Collins, Inc., USA - Myra Cohen, University of Nebraska-Lincoln, USA - Misty Davies, NASA Ames Research Center, USA - Leonardo de Moura, Microsoft, USA - Ben Di Vito, NASA Langley Research Center, USA - Alexandre Duret-Lutz, LRDE / EPITA, France - Andrew Gacek, Rockwell Collins, Inc., USA - Pierre-Loic Garoche, ONERA, France - Shalini Ghosh, SRI International, USA - Susanne Graf, Universite Joseph Fourier / CNRS / VERIMAG, France - Radu Grosu, Stony Brook University, USA - Arie Gurfinkel,SEI, Carnegie Mellon University, USA - Klaus Havelund, NASA Jet Propulsion Laboratory, USA - Constance Heitmeyer, Naval Research Laboratory, USA - Gerard Holzmann, NASA Jet Propulsion Laboratory, USA - Falk Howar, TU Clausthal / IPSSE, Germany - Rajeev Joshi, NASA Jet Propulsion Laboratory, USA - Dejan Jovanović, SRI International, USA - Gerwin Klein, NICTA and University of New South Wales, Australia - Daniel Kroening, University of Oxford, UK - Rahul Kumar, NASA Jet Propulsion Laboratory, USA - Célia Martinie, ICS-IRIT, Université Paul Sabatier, France - Eric Mercer, Brigham Young University, USA - Cesar Munoz, NASA Langley Research Center, USA - Jorge A Navas, SGT, Inc./NASA Ames Research Center, USA - Natasha Neogi, NASA Langley Research Center, USA - Ganesh Pai, SGT, Inc./NASA Ames Research Center, USA - Charles Pecheur, Université catholique de Louvain, Belgium - Lee Pike, Galois, Inc., USA - Andreas Podelski, University of Freiburg, Germany - Pavithra Prabhakar, Kansas State University, USA - Venkatesh Prasad Ranganath, Kansas State University, USA - Franco Raimondi, Middlesex University, UK - Kristin Yvonne Rozier, University of Cincinnati, USA - Neha Rungta, SGT, Inc./NASA Ames Research Center, USA - Oleg Sokolsky, University of Pennsylvania, USA - Stefano Tonetta, FBK, Italy - Helmut Veith, Vienna University of Technology, Austria - Willem Visser, Stellenbosch University, South Africa - Virginie Wiels, ONERA / DTIM, France - Guowei Yang, Texas State University, USA Steering Committee ------------------ - Julia Badger, NASA Johnson Space Center, USA - Ben Di Vito, NASA Langley Research Center, USA - Klaus Havelund, NASA Jet Propulsion Laboratory, USA - Gerard Holzmann, NASA Jet Propulsion Laboratory, USA - Michael Lowry, NASA Ames Research Center, USA - Kristin Yvonne Rozier, University of Cincinnati, USA - Johann Schumann, SGT, Inc./NASA Ames Research Center, USA

1 0

[APLS2015] 2nd Call for Participation
by Luminous Fennell 23 Nov '15

23 Nov '15

=== 2nd Call for Participation === Workshop: Advances in Programming Languages and Systems Date: December 15 - 16, 2015 Venue: Frankfurt, Germany Website: http://proglang.informatik.uni-freiburg.de/APLS2015/ Scope: ------ Advances in programming language research increasingly influence the world of software development and big software companies recognize the importance of research areas like functional programming, static program analysis, run-time verification, automated software engineering and debugging as well as automated verification techniques. This workshop is an opportunity to interact with leading international researchers in these areas, to receive crucial impulses, and to cultivate and maintain new and old collaborations and liaisons. The talks will be given by prominent members of the programming languages research community and cover a wide area of topics inside this field. The list of talks can be found below. For further information please visit http://proglang.informatik.uni-freiburg.de/APLS2015/ The workshop is sponsored by the DFG. List of talks: -------------- (Please see http://proglang.informatik.uni-freiburg.de/APLS2015/#program for further details and updates) Andreas Abel: Coinductive programming with copatterns Arthur Charguéraud: Machine-checked verification of amortized complexity analyses Dominique Devriese: Reasoning about Object Capabilities with Logical Relations and Effect Parametricity Sophia Drossopoulou: Reasoning about Programs in the Presence of Code of Unknown Provenance Joshua Dunfield: Evaluation-order Polymorphism Matthew Fluet: Type- and Control-Flow Analysis Christian Hammer: Declassification in the Browser Atsushi Igarashi: A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers Ranjit Jhala: Bounded Refinement Types Ivan Lanese: Reversible Concurrent Systems Anders Møller: Message Safety in Dart Keiko Nakata: Formal Verification of a Microkernel at FireEye James Noble: On Grace Klaus Ostermann: Automatic Refunctionalization Matthew Parkinson: The Push/Pull Model of Transactions Didier Rémy: Ornaments in ML Francesco Ranzato: Analysing Completeness in Program Analysis Ilya Sergey: Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects Jeremy Siek: A Tracing JIT for a Functional Language Wouter Swierstra: Auto in Agda Peter Thiemann: Derivatives in Program Analysis Vasco Vasconcelos: Advances in Session Types Organizers: ----------- Luminous Fennell, University of Freiburg Peter Thiemann, University of Freiburg

1 0