[TYPES/announce] PhD. Positions in Formal Methods at Royal Holloway University of London
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] PHD POSITIONS IN FORMAL METHODS Applications are invited for fully-funded PhD positions in the Department of Computer Science at Royal Holloway, University of London, awarded on the basis of academic excellence to new students who will commence a research programme in Oct 2015. We are looking for applicants interested in formal methods, particularly in one of the following areas: - Verification of first-order, higher-order, and/or concurrent software. - Automata theory - Pushdown systems and their extensions. - Higher-order recursion schemes and their extentions. - Automata models of concurrent computation - Static analysis, SMT solving, c. To discuss these areas, please contact Dr Matthew Hague (matthew.ha...@cs.rhul.ac.uk). Successful candidates will work with Dr Hague and will join his research team, see http://www.cs.rhul.ac.uk/home/hague. Scholarships are also available in the areas of - Algorithms and applications - Bioinformatics - Computer learning - Distributed and global computing - Software language engineering For more information on these areas, please see https://www.royalholloway.ac.uk/computerscience/research/home.aspx. THE DEPARTMENT OF COMPUTER SCIENCE, ROYAL HOLLOWAY UNIVERSITY OF LONDON The Department is one of the UK's leading centres for research into Computer Science. In the most recent Research Excellent Framework (REF 2014), we ranked 11th in the UK for the quality of our research output, with over 32% of our publications recognised as world leading, and a further 55% internationally excellent. The theories we develop lead to the design and building of novel practical computing systems, and their application in the real world. Research students enjoy a very lively research culture and are fully involved in the research activities of the Department (and share their successes). The Department also funds students to present their work at international conferences. INFORMATION ABOUT DEPARTMENTAL SCHOLARSHIPS A Departmental Scholarship provides support of circa 16,000 GBP per year over 3 years for a full-time student. It also includes a fee waiver to cover fees at the HEU rate. REQUIREMENTS Applicants should have a first-class honours or 2:1 degree in Computer Science or a related discipline *ADD ANY ADDITIONAL REQUIREMENTS*. Applicants should also meet English language requirements (IELTS 6.5 with no subscore lower than 5.5, or equivalent). ELIGIBILITY The scholarships are available to students starting their studies in October 2015. Home, EU and International students are eligible but please note that the scholarships do not cover overseas fees. Students who have already started their study programme are not eligible. APPLICATION PROCESS Applicants should prepare the following documents: (1) up to 4 pages proposed research topic/area and the name of a potential supervisor; (2) a brief covering letter that describes your reasons for wishing to pursue a PhD in the proposed area; (3) a copy of your CV, including your actual or expected degree class(es), and results of all University examinations; and (4) two academic references. These documents should be submitted together with an online application following the application procedure accessible from https://www.royalholloway.ac.uk/studyhere/researchdegrees/applying/home.aspx. IMPORTANT DATES March 30th 2015: scholarship application deadline Beginning of April 2015: selection interviews End of April 2015: decision of the scholarship Mid May 2015: formal confirmation of the scholarship granting For candidates who wish to fund themselves, the Department accepts applications throughout the year. The normal starting date is early October each year but alternative starting dates can be arranged. Candidates with visa requirements should ensure that they apply in time for their visa to be issued in advance of their planned start date.
[TYPES/announce] Post doc available at the IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, I have recently received a grant from the Danish Council for Independent Research to hire a post doc to work on guarded recursive types in type theory. Ideally, I would like to find someone who has both knowledge of categorical models of type theory and practical experience with proof assistants. The job is initially for one year, but with the possibility of extension for another two. Those interested should contact me. More details can be found here: https://delta.hr-manager.net/ApplicationInit.aspx?cid=119departmentId=3439ProjectId=180662MediaId=5 Rasmus Mogelberg
[TYPES/announce] CALCO 2015 : Second Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] = CALL FOR PAPERS: CALCO 2015 6th International Conference on Algebra and Coalgebra in Computer Science June 24 - 26, 2015 Nijmegen, Netherlands http://coalg.org/calco15/ == Abstract submission:March 22, 2015 Paper submission: April 2, 2015 Author notification:May 6, 2015 Final version due: June 3, 2015 == -- SCOPE -- CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science. It is a high-level, bi-annual conference formed by joining the forces and reputations of CMCS (the International Workshop on Coalgebraic Methods in Computer Science), and WADT (the Workshop on Algebraic Development Techniques). Previous CALCO editions took place in Swansea (Wales, 2005), Bergen (Norway, 2007), Udine (Italy, 2009), Winchester (UK, 2011) and Warsaw (Poland, 2013). The sixth edition will be held in Nijmegen, the Netherlands, colocated with MFPS XXXI. -- INVITED SPEAKERS -- Andy Pitts - University of Cambridge, UK (joint with MFPS) Chris Heunen - University of Oxford, UK Matteo Mio - CNRS, ENS Lyon, FR Daniela Petrisan - Radboud University, Nijmegen, NL -- TOPICS OF INTEREST -- We invite submissions of technical papers that report results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. We encourage submissions in topics included or related to those listed below. * Abstract models and logics - Automata and languages - Categorical semantics - Modal logics - Relational systems - Graph transformation - Term rewriting * Specialised models and calculi - Hybrid, probabilistic, and timed systems - Calculi and models of concurrent, distributed, mobile, and context-aware computing - General systems theory and computational models (chemical, biological, etc.) * Algebraic and coalgebraic semantics - Abstract data types - Inductive and coinductive methods - Re-engineering techniques (program transformation) - Semantics of conceptual modelling methods and techniques - Semantics of programming languages * System specification and verification - Algebraic and coalgebraic specification - Formal testing and quality assurance - Validation and verification - Generative programming and model-driven development - Models, correctness and (re)configuration of hardware/middleware/architectures, - Process algebra * Corecursion in Programming Languages - Corecursion in logic / constraint / functional / answer set programming - Corecursive type inference - Coinductive methods for proving program properties - Implementing corecursion - Applications * Algebra and Coalgebra in quantum computing - Categorical semantics for quantum computing - Quantum calculi and programming languages - Foundational structures for quantum computing - Applications of quantum algebra -- NEW TOPIC -- This edition of CALCO will feature a new topic, and submission of papers in this area is particularly encouraged. * String Diagrams and Network Theory - Combinatorial approaches - Theory of PROPs and operads - Rewriting problems and higher-dimensional approaches - Automated reasoning with string diagrams - Applications of string diagrams - Connections with Control Theory, Engineering and Concurrency -- SUBMISSION GUIDELINES -- Prospective authors are invited to submit full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. Experience papers are welcome, but they must clearly present general lessons learned that would be of interest and benefit to a broad audience of both researchers and practitioners. Starting with CALCO 2015, proceedings will be published in the Dagstuhl LIPIcsâLeibniz International Proceedings in Informatics series. Final papers should be no more than 15 pages long in the format specified by LIPIcs (http://www.dagstuhl.de/publikationen/lipics/anleitung-fuer-autoren/). It is recommended that submissions adhere to that format and length. Submissions that are clearly too long may be rejected immediately. Proofs omitted due to space limitations may be included in a clearly marked appendix. Both an abstract and the full paper must be submitted by their respective submission deadlines. A special issue of
[TYPES/announce] Postdoc Position Available
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear Colleagues, I have an opening for a postdoc, as described in the ad below. In addition to accepting applications, I am very happy to respond to informal enquiries about any aspect of the position, from technical ones to ones about life in a beautiful, alternative mountain town in western North Carolina. Best wishes, -patricia ** Applications are invited for a postdoctoral researcher in the Computer Science Department at Appalachian State University. The position is part of the NSF-funded project 'Relational Parametricity for Program Verification'. Relational parametricity is a key technique for formally verifying properties of software systems, and logical relations, upon which parametricity is based, provide a means of proving properties of a software system directly from the system itself. The goal of the project is to improve the current state-of-the-art in the theory and application of parametricity by providing an axiomatic framework for the construction of logical relations that is principled, conceptually simple, comprehensive, uniform (rather than ad hoc), predictive, and more widely applicable than already existing techniques. The ideal applicant will have a strong background in logical relations, functional programming, type theory, and category theory, although more expertise in one area may compensate for less in another. The successful applicant will also be excited about working on fundamental research questions on the themes of parametricity and language-based program verification. They will work with Prof Patricia Johann and project partners, and will also have the opportunity to initiate subprojects appropriate to their own (related) interests. The duration of the position is one year, with the possibility of continuation by mutual agreement if additional external funding is secured. The position will start at a mutually agreeable time in the second half of the 2015 calendar year. Compensation will be highly competitive and commensurate with experience. Interested persons should first contact Patricia Johann at joha...@cs.appstate.edu, briefly outlining their academic background and research interests. A complete application will consist of a cover letter and CV, including contact information for three references. Complete applications should be sent to: Patricia Johann Department of Computer Science Appalachian State University Boone, NC 28607 USA Initial review of applications will begin on 31 March 2015 and continue until the position is filled.
[TYPES/announce] PLAS 2015 Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] - Call for Papers ACM SIGPLAN Tenth Workshop on Programming Languages and Analysis for Security (PLAS 2015) Prague, Czech Republic July 2015 http://www.cs.cornell.edu/conferences/plas2015/ Co-located with ECOOP 2015 (http://2015.ecoop.org/) - Important dates 13 April 2015 (anywhere on earth): Submissions due (no extensions) 11 May 2015: Author notification 5 June 2015: Camera-ready due 6 or 7 July 2015: Workshop (The date will be assigned by the ECOOP organizers.) - PLAS aims to provide a forum for exploring and evaluating ideas on the use of programming language and program analysis techniques to improve the security of software systems. Strongly encouraged are proposals of new, speculative ideas, evaluations of new or known techniques in practical settings, and discussions of emerging threats and important problems. The scope of PLAS includes, but is not limited to: * Compiler-based security mechanisms or runtime-based security mechanisms such as inline reference monitors * Program analysis techniques for discovering security vulnerabilities * Automated introduction and/or verification of security enforcement mechanisms * Language-based verification of security properties in software, including verification of cryptographic protocols * Specifying and enforcing security policies for information flow and access control * Model-driven approaches to security * Security concerns for web programming languages * Language design for security in new domains such as cloud computing and embedded platforms * Applications, case studies, and implementations of these techniques - Submission Guidelines Two kinds of papers are invited: Full papers should be at most 12 pages long including bibliography and appendices. Papers in this category are expected to have relatively mature content. Full paper presentations will be 25 minutes each. Short papers should be at most 6 pages long including bibliography and appendices. Preliminary and exploratory work are welcome in this category. Short papers presentations will be 15 minutes each. Authors submitting papers in this category must prepend the phrase Short Paper: to the title of the submitted paper. All submissions must be in English. Page limits are strict. Submissions must be PDF documents typeset in the ACM proceedings format using 10pt fonts. A SIGPLAN-approved template can be found at the following link: http://www.sigplan.org/Resources/Author/. We recommend using this template. Both full and short papers must describe work not published in other refereed venues (see the SIGPLAN republication policy at http://www.acm.org/sigs/sigplan/republicationpolicy.htm for more details). Accepted papers will appear in workshop proceedings, which will be distributed to the workshop participants and be available in the ACM Digital Library. Submissions will be accepted through EasyChair at the following URL: https://easychair.org/conferences/?conf=plas2015. - Program Committee Stephen Chong, Harvard University Michael Clarkson (co-chair), Cornell University Christian Hammer, CISPA, Saarland University Matthew Hammer, University of Maryland, College Park Limin Jia (co-chair), Carnegie Mellon University Stephen McCamant, University of Minnesota Matteo Maffei, CISPA, Saarland University John C. Mitchell, Stanford University Toby Murray, NICTA and UNSW Benjamin C. Pierce, University of Pennsylvania Frank Piessens, KU Leuven Marco Pistoia, IBM Research Tamara Rezk, INRIA Tachio Terauchi, JAIST To reach the PC chairs, send email to plas2...@easychair.org. -
