[TYPES/announce] Two open RD engineer position in ProofInUse lab, Paris
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The new Joint Laboratory ProofInUse (funded by the French National Research Agency, see http://www.spark-2014.org/proofinuse) hires two experimented RD engineers in the domain of Formal Methods for Software Engineering. ProofInUse originates from the sharing of resources and knowledge between the Toccata research team, specializing in techniques for deductive program verification and the SME AdaCore, a software publisher, specializing in providing software development tools for critical systems. The recruited engineer will work in close collaboration with the ProofInUse Research and Development team, to address both its scientific and its technological challenges. It is expected that the engineer contributes both to advancing the academic knowledge in ProofInUse context (and thus to the production of scientific pulbications) and to the transfer of this knowledge into the software products distributed by AdaCore. We expect from the candidate some experience with Formal Methods for Software Engineering (PhD thesis or equivalent), a fair experience in software development, a plus would be the knowledge of functional programming, and the knowledge of the programming languages OCaml and Ada. More details about the scientific program and the positions are given at URL http://www.inria.fr/en/institute/recruitment/offers/r-d-engineers/%28view%29/details.html?id=PNGFK026203F3VBQB6G68LOE1LOV5=4510ContractType=6502LG=ENResultsperpage=20nPostingID=8315nPostingTargetID=14052option=52sort=DESCnDepartmentID=10 Contact: claude.mar...@inria.fr, yannick@adacore.com
[TYPES/announce] 36 month postdoc position at Bath
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] A 36-month postdoctoral research position is available at the University of Bath, to work on the EPSRC-funded project Algebra and Logic for Policy and Utility in Information Security (ALPUIS). Please send informal enquiries to Guy McCusker -- g.a.mccus...@bath.ac.uk -- and make applications via https://www.bath.ac.uk/jobs/Vacancy.aspx?ref=XVH2268 All the best, Guy McCusker. --- Research Associate - Computer Science (fixed-term) https://www.bath.ac.uk/jobs/Vacancy.aspx?ref=XVH2268 Salary: Starting from £30,728, rising to £31,664 Closing Date: Tuesday 15 April 2014 Reference: XVH2268 Applications are invited for a postdoctoral position at the University of Bath as part of the EPSRC-funded projectAlgebra and Logic for Policy and Utility in Information Security (ALPUIS). As an integral member of the ALPUIS team, you will contribute to an interdisciplinary project combining techniques from theoretical computer science (process algebra, logic) with ideas from economics (utility theory) to develop new methodologies for modeling, analyzing and making decisions about information security policy. The ALPUIS consortium comprises mathematicians, economists and policy experts from the University of Bath, University College London, the University of Aberdeen and the University of Exeter. The ideal candidate will bridge between the mathematical theory and realistic examples, producing models that reflect the theoretical development and can scale to describe and address questions of significance in security policy. Candidates should have, or shortly be expected to complete, a PhD in an area of relevance to the project. Expertise in the use of logical methods to describe and reason about the behaviour of processes or agents would be particularly desirable. Interviews will be held in April This is a fixed term post for 36 months
[TYPES/announce] 2nd CfP, VERIFY 2014, 8th Verification Workshop, *Abstract Deadline April 17th, 2014*, Focus Theme: Verification Beyond IT Systems
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies for cross posting] SECOND CALL FOR PAPERS 8th International Verification Workshop (VERIFY’14) in connection with IJCAR 2014 at FLoC 2014 July 23–24, 2014, Vienna, Austria http://vsl2014.at/verify The formal verification of critical information systems has a long tradition as one of the main areas of application for automated theorem proving. Nevertheless, the area is of still growing importance as the number of computers affecting everyday life and the complexity of these systems are both increasing. The purpose of the VERIFY workshop series is to discuss problems arising during the formal modeling and verification of information systems and to investigate suitable solutions. Possible perspectives include those of automated theorem proving, tool support, system engineering, and applications. The VERIFY workshop series aims at bringing together people who are interested in the development of safety and security critical systems, in formal methods, in the development of automated theorem proving techniques, and in the development of tool support. Practical experiences gained in realistic verifications are of interest to the automated theorem proving community and new theorem proving techniques should be transferred into practice. The overall objective of the VERIFY workshops is to identify open problems and to discuss possible solutions under the theme What are the verification problems? What are the deduction techniques? The 2014 edition of VERIFY aims for extending the verification methods for processes implemented in hard- and software to processes that may well include computer-assistance, but have a large part or a frequent interaction with non-computer-based process steps. Hence the 2014 edition will run under the focus theme Verification Beyond IT Systems A non-exclusive list of application areas with these characteristics are * Ambient assisted living * Intelligent home systems and processes * Business systems and processes * Production logistics systems and processes * Transportation logistics * Clinical processes * Social systems and processes (e.g., voting systems) The scope of VERIFY includes topics such as * ATP techniques in verification * Case studies (specification verification) * Combination of verification systems * Integration of ATPs and CASE-tools * Compositional modular reasoning * Experience reports on using formal methods * Gaps between problems techniques * Formal methods for fault tolerance * Information flow control security * Refinement decomposition * Reliability of mobile computing * Reuse of specifications proofs * Management of change * Safety-critical systems * Security models * Tool support for formal methods Submissions are encouraged in one of the following two categories: A. Regular paper: Submissions in this category should describe previously unpublished work (completed or in progress), including descriptions of research, tools, and applications. Papers must be 5-14 pages long (in EasyChair style) or 6-15 pages long (in Springer LNCS style). B. Discussion papers: Submissions in this category are intended to initiate discussions and hence should address controversial issues, and may include provocative statements. Papers must be 3-14 pages long (in EasyChair style) or 3-15 pages long (in Springer LNCS style). Important dates Abstract Submission Deadline:April 17th, 2014 Paper Submission Deadline: April 25th, 2014 Notification of acceptance: May 20, 2014 Final version due: May 27, 2014 Workshop date: July 23–24, 2014 Submission is via EasyChair: http://www.easychair.org/conferences/?conf=verify2014 Program Committee Serge Autexier (DFKI) - chair Bernhard Beckert (Karlsruhe Institute of Technology) - chair Wolfgang Ahrendt (Chalmers University of Technology) Juan Augusto (Middlesex University) Iliano Cervesato (Carnegie Mellon University) Jacques Fleuriot (University of Edinburgh) Marieke Huisman (University of Twente) Dieter Hutter (DFKI GmbH) Reiner Hähnle (Technical University of Darmstadt) Deepak Kapur (University of New Mexico) Gerwin Klein (NICTA and UNSW) Joe Leslie-Hurd (Intel Corporation) Fabio Martinelli (IIT-CNR) Catherine Meadows (NRL) Stephan Merz (INRIA Lorraine) Tobias Nipkow (TU München) Lawrence Paulson (University of Cambridge) Johann Schumann (SGT, Inc/NASA Ames) Kurt Stenzel (University of Augsburg)
[TYPES/announce] PhD opening in Proof-Theory for Multiparty Round-Trip Global Programming at IT University of Copenhagen (Deadline April 23rd)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear All, the PLUTO (Proof-Theory for Multiparty Round-Trip Global Programming) project is looking for excellent candidates for a 3/4-year PhD scholarship. Successful applicants have a background in theoretical computer science, with particular focus on concurrency theory, type theory, logic and proof assistants. *Highlights:* *- Application deadline: **23th April 2014, at 23:59 CET.* *- Application link: * https://delta.hr-manager.net/ApplicationInit.aspx?cid=119ProjectId=168671departmentId=3439uiculture=enMediaId=1282 - *Contact*: Marco Carbone (carbo...@itu.dk), IT University of Copenhagen - *Scholarship*: full scholarship, including full time salary and funding for travels. - *Research Environment: *Programming, Logic and Semantics ( www.itu.dk/research/pls) research group @IT University of Copenhagen, Denmark *Project Description: *Computing systems consist of several, distributed entities that communicate by message exchange. The increasing complexity of such systems poses a challenge on how to program them correctly. Recent research proposed global programming, a new paradigm for preventing typical distributed software errors, where systems are programmed with global descriptions of how messages are exchanged, rather than giving the local behaviour of each of their endpoints. Unfortunately, global programming does not yet support modular development and integration with existing legacy software. The objective of this project is to address these issues by developing the foundations for modular round-trip engineering of global programs, called round-trip global programming: global programs are mapped to endpoint code, composed with existing, legacy software, and the resulting composition can be translated back to a new overall global program. **The available positions also depend on pending funding from The Danish Council for Independent Research** -- Marco Carbone Associate Professor IT University of Copenhagen Rued Langgaards vej 7 2300 Copenhagen Denmark Phone: +45 7218 5067 Email: carbo...@itu.dk Home: http://www.itu.dk/people/maca
[TYPES/announce] Second call for papers: APAL special issue on games for logic and programming languages
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] ANNALS OF PURE AND APPLIED LOGIC (APAL) SPECIAL ISSUE ON GAMES FOR LOGIC AND PROGRAMMING LANGUAGES CALL FOR PAPERS TOPIC 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 effects such as control, references or concurrency. Nowadays, game semantics has expanded to a variety of fields in theory and analysis of computation, such as theories of concurrency, semantics of lambda calculi and proofs, program analysis, model checking and hardware synthesis. This special issue, based on the GALOP workshop held at Queen Mary University of London in 2013 (seehttp://www.gamesemantics.org/galop-viii), aims to reflect new developments in this area. Topics of interest for contributions to the journal issue include, but are not limited to game semantics and its applications to: - Game theory and interaction models in semantics - Games-based program analysis and verification - Logics for games and games for logics - Algorithmic aspects of games - Categorical aspects - Programming languages and full abstraction - Higher-order automata and Petri nets - Geometry of Interaction - Ludics - Epistemic game theory - Logics of dependence and independence - Computational linguistics SUBMISSIONS Submissions must be original work, which has not been previously published in a full form and is not currently under review for publication elsewhere. Please submit submissions following APAL's style (http://authors.elsevier.com/JournalDetail.html?PubID=505603) on the following easychair link: https://www.easychair.org/conferences/?conf=apalgalop2013 The deadline for submission is May 31st, 2014. GUEST EDITORS Martin Hyland (University of Cambridge) Guy McCusker (University of Bath) Nikos Tzevelekos (Queen Mary University of London)
[TYPES/announce] Oregon PL Summer School: call for participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] This year's Oregon Programming Languages Summer School will take place from June 16th to 28th, 2014. The registration deadline is April 14th. Full information on registration and scholarships an be found here: http://www.cs.uoregon.edu/Activities/summerschool The school has a long and successful tradition (sponsored by the NSF, ACM SIGPLAN, and industry). It covers current research in the theory and practice of programming languages. Material is presented at a tutorial level that will help graduate students and researchers from academia or industry understand the critical issues and open problems confronting the field. Prerequisites are an elementary knowledge of logic and mathematics, as covered in undergraduate classes on discrete mathematics, and some knowledge of programming languages at the level of an undergraduate survey course. This year we will again offer a Coq boot camp session, to be held on June 15th -- one day before the summer school officially begins. The boot camp will provide a one-day, intensive, hands-on introduction to the practical mechanics of the Coq proof assistant. The Coq boot camp will be run by Michael Clarkson (George Washington University). More information is available at the above website. This year's program is titled Types, Logic, Semantics, and Verification. The speakers and topics include: Andrew Appel -- Software Verification Princeton University Lars Birkedal -- Category Theory Aarhus University Derek Dreyer -- Modular Reasoning about Stateful Programs Max Planck Institute for Software Systems Robert Harper -- Type Theory Foundations Carnegie Mellon University Greg Morrisett -- Certified Programming and State Harvard University Ulf Norell -- Programming in Agda Chalmers University of Technology Brigitte Pientka -- Proof Theory Foundations McGill University Stephanie Weirich -- Designing Dependently-Typed Programming Languages University of Pennsylvania Steve Zdancewic -- Software Foundations in Coq University of Pennsylvania We hope you can join us for this excellent program! Amal Ahmed Zena Ariola Greg Morrisett OPLSS 2014 organizers
[TYPES/announce] PhD studentship in data-centric programming at LFCS, University of Edinburgh
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] A fully-funded 3-year PhD studentship has become available in LFCS in data- centric programming. Applications and expressions of interest are welcome now, with a closing date of April 28, 2014. This studentship is partly funded by a EU FP7 project (DIACHRON) and partly by a Google Research Award. The funding includes UK/EU tuition and fees, and a non-taxable stipend of approximately £13,800 per year for 3 years; a small amount of additional funding is available that may be used flexibly for equipment, travel or additional stipend support. The topic of the studentship is flexible within the general area of data-centric programming languages; possible topics include: * Types and language design for integrating multiple data-centric programming models (e.g. language-integrated database query, GPU, or MapReduce programming) * Extending bidirectional programming for synchronizing data across datamodels * Language-based techniques for data curation and preservation, provenance tracking, or archiving * Query and update techniques for longitudinal or provenance-aware queries. (http://wcms.inf.ed.ac.uk/lfcs/graduate%20study/data-centric-programming -and-provenance) A strong candidate for this studentship will have, or expect to receive, a first-class undergraduate degree or a strong performance in a master's degree. She or he should also be familiar with foundations of programming languages and databases, expert in at least one of these areas, and excited about research in this fast-moving area. The student will benefit from LFCS's strong research groups in both Programming Languages and Databases, from Scotland's active programming languages research community, and from proximity to Edinburgh's Centres for Doctoral Training on Pervasive Parallelism or Data Science, which offer 4-year combined Master's + PhD programs and have strong links to industry forming the basis for internships. It may be possible for us to offer the successful applicant an additional year of funded study through one of these programs. == Application instructions == The application deadline is April 28, 2014. Applications will be reviewed on a rolling basis as they are received and an offer will be made to the strongest candidate as soon as possible after the closing date. Due to restrictions on the funding, applicants with UK/EU citizenship or residence will be prioritized. Please get in touch early in case of questions about the application process, project ideas or study in the UK or Edinburgh. Current applicants to other Edinburgh PhD programs can be considered for this funding. If you are interested in this project and your application to another Edinburgh PhD program is currently under review, please contact me (jche...@inf.ed.ac.uk) to discuss how to proceed. To apply, please follow the instructions at: http://wcms.inf.ed.ac.uk/lfcs/graduate%20study/apply/ == About the University of Edinburgh and LFCS == The University of Edinburgh School of Informatics brings together world-class research groups in theoretical computer science, artificial intelligence and cognitive science. The School led the UK 2008 RAE rankings in volume of internationally recognised or internationally excellent research. The Laboratory for Foundations of Computer Science was established by Burstall, Milner and Plotkin in 1986, and is recognized worldwide for groundbreaking research on topics in programming languages, semantics, type theory, proof theory, algorithms and complexity, databases, security, and systems biology. Programming Languages and Foundations is one of the largest research activities in LFCS, including 15 academic staff, 9 postdoctoral researchers and 6 current PhD students. We participate in a thriving PL research community across Scotland, with Scottish ProgrammingLanguages Seminars hosted every 3-4 months by PL groups at Glasgow, Strathclyde, Heriot-Watt, St. Andrews, Dundee and Edinburgh. For more information about Edinburgh and studying here, see these pages: * Explore Edinburgh (http://www.ed.ac.uk/about/city) * Overview for prospective postgraduates (http://www.ed.ac.uk/schools-departments/informatics/postgraduate) * Programming Languages and Foundations at LFCS (http://wcms.inf.ed.ac.uk/lfcs/research/groups-and-projects/pl) * Edinburgh Database Group (https://wcms.inf.ed.ac.uk/lfcs/research/groups-and-projects/database)
[TYPES/announce] PSC 2014 Call for papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Proof, Structure, and Computation 2014 CSL-LICS Workshop July 17-18, 2014, Vienna, Austria http://vsl2014.at/psc/ === Highlights === - PSC welcomes submissions of short abstracts: 1-2 pages in LNCS format - Invited speakers: Ulrich Berger and Martin Escardo - Post-proceedings are planned for a journal special issue === Important Dates === 1 May 2014.. Abstract submission 16 May 2014... Notification to authors 16 June 2014.. Camera-ready abstracts for electronic proceedings 17-18 July 2014. PSC in Vienna === Scope === The extraction of computational content from proofs has a long tradition in logic, but usually depends on a concrete encoding that allows us to turn proofs into algorithms. A recent trend in this field is the departure from such encoding which not only makes it simpler to represent the mathematical content, but also makes the extracted computational content encoding independent. This shift in focus allows us to focus on what is relevant: the computational aspects of proofs and the specification (not representation) of the structures involved. We now have growing evidence that this move from representations (e.g. the signed digit representation of the reals) to axioms (e.g. of the real numbers) is possible. This development largely parallels the step from assembler to high level languages in programming. As a by-product this move has already opened up the possibility to gain computational information from axiomatic proofs in more abstract and genuinely structural areas of mathematics such as algebra and topology. === Invited Speakers === Ulrich Berger (Swansea University, UK) Martin Escardo (University of Birmingham, UK) === Submissions === We welcome 1-2-page abstracts presenting (finished, ongoing, or if clearly stated even published) work on proof, structure, and computation. Particular topics of interest are - Proof Theory - Program Extraction - Constructive Mathematics - Topology and Computation - Realisability Semantics - Coalgebra and Computation - Categorical Models - Domain Theory - Interval Analysis === Submission Guidelines === Abstracts are invited of ongoing, finished, or (if clearly stated) even published work on a topic relevant to the workshop. The abstracts will appear in electronic pre-proceedings that will be distributed at the meeting. Abstracts (at most 2 pages, in LNCS style) are to be be submitted electronically in PDF via EasyChair (http://www.easychair.org/conferences/?conf=psc2014)http://www.easychair.org/conferences/?conf=ice2014 . Accepted communications must be presented at the workshop by one of the authors. === Special Issue === We plan to invite extended versions of selected abstract with original work to post-proceedings in a journal special issue. They will be peer-reviewed according to the standard journal policy. === Program Committee === Neil Ghani (University of Strathclyde, UK) Helle Hvid Hansen (Radboud University Nijmegen, NL) Rosalie Iemhoff (Utrecht University, NL) Bjoern Lellmann (TU Vienna, AT) Sara Negri (University of Helsinki, FI) Dirk Pattinson (ANU, AU), PC chair Dieter Probst (University of Bern, CH) Peter Schuster (University of Leeds, UK), PC chair Alex Simpson (University of Edinburgh, UK) Ana Sokolova (University of Salzburg, Austria), PC chair === Organizing Committee === Dirk Pattinson (ANU, Australia), PC chair Peter Schuster (University of Leeds, UK), PC chair Ana Sokolova (University of Salzburg, Austria), PC chair === Contact === psc2...@easychair.org
