[TYPES/announce] Multiple Research Fellow positions at the Australian National University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies for multiple postings] Dear Colleagues, we have multiple Research Fellow positions at the School of Computing, the Australian National University; see below for details. Please feel free to forward this to those interested. Regards, -Alwen Research Fellow (multiple positions) School of Computing, the Australian National University. Salary package: Level B, A$99,809 – A$113,165 per annum plus 17% superannuation Term: Fixed Term (2-3 years)] Postdoctoral Research Position - opportunity to build own research agenda - embedded in diverse team - several positions available, depending on the knowledge and interest of the applicant The Research Fellow will develop foundations and tools for specifying and verifying software, with a particular emphasis on applications in the areas of concurrency, programming languages, and security. Foundations should be based on sound mathematical frameworks, e.g., process algebra or operational semantics. Tool support can range from frameworks within interactive proof assistants via the use of off-the-shelf model checkers to code generation. The Postdoctoral Fellow should apply the developed theory to real-world case studies, such as compiler verification, or the analysis of protocols in terms of correctness or security. The successful candidate is encouraged to develop new and innovative research directions in their specified scientific impact domain, including relevant collaborations. Please see jobs.anu.edu.au/cw/en/job/543320 for more details. Review of your application is guaranteed if your application is received by *31 January 2022.* The search will continue until the positions are filled, or until *30 June 2022*, whichever comes first.
[TYPES/announce] LFMTP 2020 Post-Proceedings: Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies if you received multiple copies of this CFP] CALL FOR PAPERS Logical Frameworks and Meta-Languages: Theory and Practice (Post-Proceedings) LFMTP 2020 https://lfmtp.org/workshops/2020/ Abstract submission deadline: 2 October 2020 Paper submission deadline: 9 October 2020 ABOUT LFMTP Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process. The LFMTP 2020 workshop adopts a post-proceedings publication model. The workshop itself took place on 29-30 June 2020 online, jointly with IJCAR and FSCD. Now that the workshop has concluded, we solicit submissions of full papers for the post-proceedings of LFMTP 2020, which will go through the normal peer-review process. Submission is open to all; attendance at the workshop is not prerequisite. Submissions related to the following topics are welcome: * Encoding and reasoning about the meta-theory of programming languages, process calculi and related formally specified systems. * Formalisation of model-theoretic and proof-theoretic semantics of logics. * Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Logical treatments of inductive and co-inductive definitions and associated reasoning techniques, including inductive types of higher dimension in homotopy type theory. * Graphical languages for building proofs and their applications in geometry, equational reasoning and category theory. * New theory contributions: canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, homotopy and cubical type theory. * Applications of logical frameworks: proof-carrying architectures, proof exchange and transformation, program refactoring, etc. * Techniques for programming with binders in functional programming languages such as Haskell, OCaml or Agda, and logic programming languages such as lambda Prolog or Alpha-Prolog. * Design and implementation of systems and tools related to meta-languages and logical frameworks IMPORTANT DATES All deadlines are established as the end of day (23:59) AoE. * Abstract submission deadline: 2 October 2020 * Paper submission deadline: 9 October 2020 * Notification to authors: 20 November 2020 * Final version due: 4 December 2020 SUBMISSION INFORMATION Submitted papers should be in PDF, formatted using the EPTCS LaTeX style. The length is restricted to 15 pages. Submission is via EasyChair: https://easychair.org/my/conference?conf=lfmtp2020 All submissions will be peer-reviewed and accepted papers will be published in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series. PROGRAM COMMITTEE David Baelde, LSV, ENS Paris-Saclay & Inria Paris Frédéric Blanqui, INRIA Alberto Ciaffaglione, University of Udine Dennis Müller, Friedrich-Alexander-University Erlangen-Nürnberg Michael Norrish, Data61 Carlos Olarte, Universidade Federal do Rio Grande do Norde Claudio Sacerdoti Coen, University of Bologna (PC Co-Chair) Ulrich Schöpp, fortiss GmbH Alwen Tiu, Australian National University (PC Co-Chair) Tjark Weber, Uppsala University
[TYPES/announce] Research Fellow Position at the Australian National University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies for multiple postings] A two-year Research Fellow position is available at the Research School of Computer Science at the Australian National University (ANU). The position is for a project on massively scaling automated verification techniques for security protocol verification. Of particular interests are techniques to scale up verification for equivalence properties of security protocols (covering eg, anonymity, unlinkability, etc). This project will investigate the use of high performance computing (HPC) platform to massively parallelise the verification algorithms. The deadline for application is 31 January 2020 (11:55pm, Australian Eastern Time). Salary range is A$99,809 - A$113,165 (roughly, US$ 68K - US$ 77K, or 61K Euros - 70K Euros). Applicants with strong backgrounds in formal methods (SAT/SMT, first-order theorem proving, interactive theorem provers) and programming languages are preferred. Experience with implementation of theorem provers is desirable. Details of the application procedure can be found at: https://jobs.anu.edu.au/en/job/534934/research-fellow For further information please contact Alwen Tiu (alwen.tiu at anu.edu.au). Regards, Alwen Tiu
[TYPES/announce] Call for Papers: APLAS 2019
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies for multiple posts] CALL FOR PAPERS 17th Asian Symposium on Programming Languages and Systems (APLAS’19) Dec 2-4, 2019 Bali, Indonesia Website: https://conf.researchr.org/home/aplas-2019 The 17th Asian Symposium on Programming Languages and Systems (APLAS19; https://conf.researchr.org/home/aplas-2019) aims to stimulate programming language research by providing a forum for the presentation of the latest results and the exchange of ideas in programming languages and systems. APLAS is based in Asia but is an international forum that serves the worldwide programming languages community. APLAS 2019 will be held in Hotel Melia, Bali (Nusa Dua), Indonesia on 2 - 4 December 2019. Papers are solicited on topics such as: - Semantics, logics, foundational theory - Design of languages, type systems, and foundational calculi - Domain-specific languages - Compilers, interpreters, abstract machines - Program derivation, synthesis, and transformation - Program analysis, verification, model-checking - Logic, constraint, probabilistic, and quantum programming - Software security - Concurrency and parallelism - Tools and environments for programming and implementation Topics are not limited to those discussed in previous symposiums. Papers identifying future directions of programming and those addressing the rapid changes of the underlying computing platforms are especially welcome. Demonstration of systems and tools in the scope of APLAS are welcome to the System and Tool demonstrations category. Authors concerned about the appropriateness of a topic are welcome to consult with program chair prior to submission. IMPORTANT DATES Abstract deadline: June 11, 2019 (anywhere on Earth) Submission deadline: June 14, 2019 Author response: July 24-26, 2019 Author notification: August 12, 2019 Final version: August 30, 2019 Conference: December 2 - 4, 2019 CALL FOR REGULAR RESEARCH PAPERS We solicit submissions in the form of regular research papers describing original scientific research results, including system development and case studies. Regular research papers should not exceed 18 pages in the Springer LNCS format, including bibliography and figures. This category encompasses both theoretical and implementation (also known as system descriptions) papers. In either case, submissions should clearly identify what has been accomplished and why it is significant. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. System descriptions papers should contain a link to a working system and will be judged on originality, usefulness, and design. In case of lack of space, proofs, experimental results, or any information supporting the technical results of the paper could be provided as an appendix or a link to a web page, but reviewers are not obliged to read them. CALL FOR TOOL PAPERS We solicit submissions in the form of tool papers describing a demonstration of a tool or a system that support theory, program construction, reasoning, or program execution in the scope of APLAS. The main purpose of a tool paper is to display a completed, robust and well-documented tool-highlighting the overall functionality of the tool, the interfaces of the tool, interesting examples and applications of the tool, an assessment of the tool’s strengths and weaknesses, and a summary of documentation/support available with the tool. Authors of tool demonstration proposals are expected to present a live demonstration of the tool at the conference. It is highly desirable that the tools are available on the web. System and Tool papers should not exceed 8 pages in the Springer LNCS format, including bibliography and figures. They may include an additional appendix of up to 6 extra pages giving the outline, screenshots, examples, etc. to indicate the content of the proposed live demo. SUBMISSION INFORMATION Papers should be submitted electronically via the submission web page using EasyChair (https://easychair.org/my/conference?conf=aplas19). The acceptable format is PDF. Submitted papers must be unpublished and not submitted for publication elsewhere. Papers must be written in English. The proceedings will be published as a volume in Springer’s LNCS series. Accepted papers must be presented at the conference. REVIEW PROCESS APLAS 2019 will use a lightweight double-blind reviewing process. Following this process means that reviewers will not see the authors’ names or affiliations as they initially review a paper. The authors’ names will then be revealed to the reviewers only once their reviews have been submitted. To facilitate this process, submitted papers must adhere to the following: Author names and institutions must be omitted and References to the authors’ own related work should be in the third person (e.g., not “We build on our previous work …” but rather “We
Re: [TYPES/announce] Postdoc position on security protocol verification at NTU Singapore
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Apology for multiple postings. There was a typo in the previous posting regarding the application deadlines. Below is the corrected version. Regards, -Alwen -- One postdoc position is available at the School of Computer Engineering, Nanyang Technological University (NTU) Singapore, for a project on verification of security protocols funded by the Ministry of Education of Singapore. A particular emphasis will be on designing and implementing decision procedures for finding attacks on protocols or producing formal proofs of their security. We will be using a mixture of process algebraic and logical frameworks to express protocols and their properties, in particular, equivalence properties of security protocols. Candidates must possess a PhD degree in Computer Science or related areas. Candidates with strong backgrounds in process calculus, such as the pi-calculus and its variants, and/or formal logic and theorem proving are preferred. The salary range is between SGD 4000 - 6000 per month. The position will be initially offered for one year, but can be extended up to three years, subject to satisfactory performance and availability of funding. To apply for the position, please send a cover letter and your latest CV (please indicate names of three referees in your CV) by email to Alwen Tiu ( a...@ntu.edu.sg, alwen@gmail.com). Applications will be accepted until the position is filled, but to ensure the full consideration of your application, please send your application by 21 February 2016. Only shortlisted candidates will be notified of the results of their applications. The selected candidate is expected to commence in April 2016. If you have any further questions regarding the position and/or the project, please email a...@ntu.edu.sg. Regards, Alwen Tiu
[TYPES/announce] Postdoc position on security protocol verification at NTU Singapore
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] One postdoc position is available at the School of Computer Engineering, Nanyang Technological University (NTU) Singapore, for a project on verification of security protocols funded by the Ministry of Education of Singapore. A particular emphasis will be on designing and implementing decision procedures for finding attacks on protocols or producing formal proofs of their security. We will be using a mixture of process algebraic and logical frameworks to express protocols and their properties, in particular, equivalence properties of security protocols. Candidates must possess a PhD degree in Computer Science or related areas. Candidates with strong backgrounds in process calculus, such as the pi-calculus and its variants, and/or formal logic and theorem proving are preferred. The salary range is between SGD 4000 - 6000 per month. The position will be initially offered for one year, but can be extended up to three years, subject to satisfactory performance and availability of funding. To apply for the position, please send a cover letter and your latest CV (please indicate names of three referees in your CV) by email to Alwen Tiu ( a...@ntu.edu.sg, alwen@gmail.com). Applications will be accepted until the position is filled, but to ensure the full consideration of your application, please send your application by 21 August 2015. Only shortlisted candidates will be notified of the results of their applications. The selected candidate is expected to commence in October 2015. If you have any further questions regarding the position and/or the project, please email a...@ntu.edu.sg. Regards, Alwen Tiu
[TYPES/announce] One postdoc and two PhD positions on formal verification of security protocols
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies for multiple postings] One postdoc and two PhD positions are available at the School of Computer Engineering, Nanyang Technological University (NTU) Singapore. The postdocs and the PhDs positions are for a project on verification of security protocols funded by the Ministry of Education of Singapore. A particular emphasis will be on designing and implementing decision procedures for finding attacks on protocols or producing formal proofs of their security. We will be using a mixture of process algebraic and logical frameworks to express protocols and their properties. For the postdoc position: = Candidates must possess a PhD degree in Computer Science or related areas. Candidates with strong backgrounds in process calculus, such as the pi-calculus and its variants, and/or formal logic and theorem proving are preferred. For further details, including the salary range, please refer to the job ads at: https://www.jobsbank.gov.sg/ICMSPortal/portlets/JobBankHandler/SearchDetail.do?id=JOB-2015-0238754 The position will be initially offered for one year, but can be extended up to three years, subject to satisfactory performance and availability of funding. To apply for the position, please send a cover letter and your latest CV (please indicate names of three referees in your CV) by email to Alwen Tiu ( a...@ntu.edu.sg, alwen@gmail.com). Applications will be accepted until the position is filled, but to ensure the full consideration of your application, please send your application by 21 August 2015. Only shortlisted candidates will be notified of the results of their applications. The selected candidate is expected to commence in October 2015. For the PhD positions: == please send an email to Alwen Tiu (a...@ntu.edu.sg) to express your interests. Please refer to the following website for application procedures and requirements. For the intake of January 2016, applications must be received by 31 August 2015. http://admissions.ntu.edu.sg/graduate/Pages/home.aspx If you have any further questions, please contact a...@ntu.edu.sg. Regards, Alwen Tiu
[TYPES/announce] CPP 2015: second call for papers
Alwen Tiu (co-chair), Nanyang Technological University, Singapore Stephanie Weirich , University of Pennsylvania, USA
[TYPES/announce] Call for Papers: Certified Programs and Proofs (CPP) 2015
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The 4th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2015) Mumbai, India, 12 - 14 January 2015 http://cpp2015.inria.fr Co-located with POPL 2015 (http://popl.mpi-sws.org/2015/) Call for Papers === CPP is an international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. CPP 2015 is the fourth in the CPP conference series and will be co-located with POPL 2015 in Mumbai from 12 - 14 January 2015. Important dates Abstract submission: 3 October 2014, anywhere on Earth (11:59 pm, UTC-12) Full paper submission:10 October 2014, anywhere on Earth (11:59 pm, UTC-12) Notification: 29 November 2014 Camera-ready deadline:15 December 2014 Conference dates:12 - 14 January 2015 Scope -- Suggested, but not exclusive, specific topics of interest for submissions include: - certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors; - program logics, type systems, and semantics for certified code; - certified decision procedures, mathematical libraries, and mathematical theorems; - proof assistants and proof theory; - new languages and tools for certified programming; - program analysis, program verification, and proof-carrying code; - certified secure protocols and transactions; - certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; - certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; - certificates for program termination; - logics for certifying concurrent and distributed programs; - higher-order logics, logical systems, separation logics, and logics for security; - teaching mathematics and computer science with proof assistants. Submission instructions --- Submitted papers should not exceed 12 pages in the ACM SIGPLAN Proceedings format. Shorter papers are welcome and will be given equal consideration. The proceedings of the conference will be published by the ACM. Templates for ACM SIGPLAN format can be found on the ACM SIGPLAN website: http://www.sigplan.org/Resources/Author. Papers should be submitted in PDF format, through the EasyChair submission page: https://www.easychair.org/conferences/?conf=cpp2015 Each submission must be written in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference, all phrased for the non-specialist. Technical and formal developments directed to the specialist should follow. Whenever appropriate, the submission should come along with a formal development, using whatever prover, e.g., Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS, Vampire, etc. References and comparisons with related work should be included. Papers not conforming to the above requirements concerning format and length may be rejected without further consideration. The results must be unpublished and not submitted for publication elsewhere, including the proceedings of other published conferences or workshops. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. Original formal proofs of known results in mathematics or computer science are among the targets. One author of each accepted paper is expected to present it at the conference. Program Committee - Andreas Abel, Chalmers and Gothenburg University, Sweden June Andronick, NICTA and UNSW, Sydney, Australia Nick Benton, Microsoft Research, Cambridge, UK Lennart Beringer, Princeton University, USA James Brotherston. University College London, UK Kaustuv Chaudhuri, Inria, Saclay, France Amy Felty, University of Ottawa, Canada Chung-Kil Hur , Seoul National University, Korea Naoki Kobayashi, University of Tokyo, Japan Xavier Leroy (co-chair), Inria, Paris-Rocquencourt, France Leonardo de Moura , Microsoft Research, Redmond, USA Magnus Myreen , University of Cambridge, UK Vivek Nigam, Federal University of Paraíba, Brasil Tobias Nipkow, Technische Universität München. Germany Christine Paulin-Mohring, Université Paris-Sud, France Natarajan Raja, Tata Institute of Fundamental Research, Mumbai, India Gert Smolka, Saarland University, Germany Alwen Tiu (co-chair), Nanyang Technological University, Singapore Stephanie Weirich , University
[TYPES/announce] Postdoc position at the Australian National University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Apologies for multiple postings. - [http://info.anu.edu.au/hr/Jobs/Academic_Positions/_CECS4727.asp] Employment Position Available ANU College of Engineering and Computer Science Research School of Information Sciences and Engineering Computer Sciences Laboratory Research Fellow Fixed Term – 2 years Academic Level B Salary Package: $68,767 - $81,135 pa plus 17% super Reference No.: CECS4727 The Computer Sciences Laboratory seeks to fill a research position to work with, and under the direction of, Dr Alwen Tiu. The position is for a project in the area of computer science, funded by the Australian Research Council (ARC) under the Discovery Projects funding scheme. The research will involve applications of proof theory to reason about process calculi, such as the pi-calculus and its extensions, with a focus on the mechanisation of equivalence checking. The appointee is expected to have a PhD degree in computer science, with backgrounds in proof theory, theorem proving, and process calculi, in particular, the pi-calculus and its extensions. Backgrounds in related area such as type theory and programming languages are a plus. The appointment will be for two years, starting in September 2008. Further particulars, including selection criteria, are available from: Reception, RSISE, phone +61 2 6125 8821, e-mail [EMAIL PROTECTED] or http://info.anu.edu.au/hr/Jobs/Academic_Positions/_PDF/CECS4727.pdf. If you wish to discuss the position after obtaining the selection documentation, please contact: Dr Alwen Tiu, phone +61 2 6125 5992, e-mail [EMAIL PROTECTED] Information for applicants http://info.anu.edu.au/hr/Jobs/How_To_Apply/index.asp. Job Application Cover sheet - http://info.anu.edu.au/policies/_DHR/Forms/HR86.asp. *Closing Date:* 1 May 2008
