[TYPES/announce] Postdoc position at Paris Diderot University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] RAPIDO -- Reasoning And Programming with Infinite Data-Objects. (http://www.irif.fr/~saurin/RAPIDO) * postdoc positions in RAPIDO project: We are opening a post-doc position in RAPIDO project, which is aimed at studying logical methods and tools for enhancing reasoning and programming on infinite data. The post-doc would start sometimes during the fall 2018 (start date between october 2018 and january 2019). RAPIDO is an ANR-funded project hosted at Paris Diderot University involving researchers from three french labs: IRIF (Univ Paris Diderot), LIP (ENS Lyon) and LSV (ENS Paris Saclay). It is coordinated by Alexis Saurin (IRIF lab, sau...@irif.fr) and the post-doc position will administratively be hosted by Paris Diderot University. RAPIDO aims at gathering young researchers to investigate the applicability of proof-theoretical methods to reason and program on infinite data objects. The goal of the project is to develop logical systems capturing infinite proofs (proof systems with least and greatest fixed points as well as infinitary proof systems), to design and to study programming languages for manipulating infinite data such as streams both from a syntactical and semantical point of view. Moreover, the ambition of the project is to apply the fundamental results obtained from the proof- theoretical investigations (i) to the development of software tools dedicated to the reasoning about programs computing on infinite data, e.g. stream programs (more generally coinductive programs), and (ii) to the study of properties of automata on infinite words and trees from a proof-theoretical perspective with an eye towards model-checking problems. * Topics and requirements for applicants We are looking for young researchers who can contribute to the research topics of RAPIDO. Candidates should hold a PhD in computer science or a closely related field (or be close to complete their PhD) with skills in formal methods and logic and a strong expertise in at least one of the following topics: * automata theory, coinduction, cyclic and infinitary proofs, denotational semantics, functional programming, games and game semantics, infinitary rewriting, lazy evaluation, linear logic, MSO logic, proof assistants, proof theory, realizability, streams, temporal logics. * We will be particularly interested in applications of candidates having an experience using the Coq proof assistant, but this is not a requirement for applying! * Important dates: Informal enquiries: as soon as possible Application deadlines: july 18th 2018 Starting date: between october 2018 and january 2019. * Application submission guidelines Applications should be sent to Alexis Saurin before July 18th 2018 in an email entitled "RAPIDO postdoc application", providing: - a detailed CV with a publication list, - a research statement of at most two pages plus bibliography, - and one or two recommendation letters. Potential candidates are strongly encouraged to contact the project coordinator (together with other project members) for informal enquiries as soon as the announcement is released, and at least when *starting* preparing their application (for info on topics such as starting dates, connections with project sites, salary...). More informations on the post-doc position available at: https://www.irif.fr/~saurin/RAPIDO/files/post-doc-announcement-2018.txt Best, Alexis -- Alexis Saurin CNRS researcher, IRIF
[TYPES/announce] PPDP 2018: Call for Participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] == PPDP 2018: Call for Participation == 20th International Symposium on Principles and Practice of Declarative Programming Frankfurt am Main, Germany, 3-5 September 2018 http://ppdp-lopstr-18.cs.uni-frankfurt.de/ppdp18.html (co-located with LOPSTR 2018 and WFLP 2018) http://ppdp-lopstr-18.cs.uni-frankfurt.de == Registration http://www.ppdp-lopstr-18.cs.uni-frankfurt.de/#registration Early registration ends on 15 August, 2018. Session in Honour of Martin Hofmann === PPDP will include a session in honour of Martin Hofmann including a talk given by Nick Benton, Facebook on Semantic Equivalence Checking for HHVM Bytecode Invited Talks = - Philippa Gardner, Imperial College. Testing and Verification for JavaScript (joint with LOPSTR) - Jorge Navas, SRI International. Constrained Horn Clauses for Verification (joint with LOPSTR) - Chung-Chieh Shan, University of Indiana. Calculating Distributions Accepted Papers === - Maciej Bendkowski and Pierre Lescanne. Combinatorics of explicit substitutions - Manfred Schmidt-Schauss, David Sabel and Nils Dallmeyer. Sequential and Parallel Improvements in a Concurrent Functional Programming Language - Magnus Madsen and Ondrej Lhotak. Implicit Parameters for Logic Programming - Mistral Contrastin, Dominic Orchard and Andrew Rice. Automatic reordering for dataflow safety of Datalog - Danil Annenkov and Martin Elsman. Certified Compilation of Financial Contracts - José Fragoso Santos, Petar Maksimović, Théotime Grohens, Julian Dolby and Philippa Gardner. Cosette: Symbolic Execution for JavaScript - Michael Hanus. Verifying Fail-Free Declarative Programs - Dmitri Rozplokhas and Dmitry Boulytchev. Improving Refutational Completeness of Relational Search via Divergence Test - Martin Sulzmann and Kai Stadtmüller. Two-Phase Dynamic Analysis of Message-Passing Go Programs based on Vector Clocks - Sylvia Grewe, Sebastian Erdweg, André Pacak and Mira Mezini. An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers - Gopalan Nadathur and Yuting Wang. Schematic Polymorphism in the Abella Proof Assistant - Stephan Adelsberger, Anton Setzer and Eric Walkingshaw. Declarative GUIs: Simple, Consistent, and Verified - Genki Sakanashi and Masahiko Sakai. Transformation of combinatorial optimization problems written in extended SQL into constraint problems - Yuki Nishida and Atsushi Igarashi. Nondeterministic Manifest Contracts - Alberto Pardo, Emmanuel Gunther, Miguel Pagano and Marcos Viera. An Internalist Approach to Correct-by-Construction Compilers - Falco Nogatz, Jona Kalkus and Dietmar Seipel. Web-based Visualisation for Definite Clause Grammars using Prolog Meta-Interpreters - Helmut Seidl and Ralf Vogler. Three improvements to the top-down solver - Flavien Breuvart and Ugo Dal Lago. On Intersection Types and Probabilistic Lambda Calculi - Taku Terao. Lazy Abstraction for Higher-Order Program Verification - Maximiliano Klemen, Nataliia Stulova, Pedro Lopez-Garcia, Jose F. Morales and Manuel V. Hermenegildo. Static Performance Guarantees for Programs with Run-time Checks - Abhishek Dang and Piyush Kurur. Verse: An EDSL for cryptographic primitives - Pablo Barenbaum, Eduardo Bonelli and Kareem Mohamed. Pattern Matching and Fixed Points: Resources Types and Strong Call-By-Need Sponsors PPDP is financially supported by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - 407531063, and by the Goethe-University Frankfurt am Main. Conference Organisers = Program Committee See http://www.ppdp-lopstr-18.cs.uni-frankfurt.de/ppdp18.html#pc Program Chair Peter Thiemann, Universität Freiburg, Germany Organizing Committee (Goethe-University Frankfurt am Main, Germany) Ehud Cseresnyes Nils Dallmeyer Bircan Dölek Ronja Düffel Lars Huth Leonard Priester David Sabel (General Chair)
[TYPES/announce] PhD Position in ICT in Trento on "Quantum Annealing for SAT Solving"
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] -- [ We apologize if you receive multiple copies of this message] PLEASE FORWARD THIS EMAIL TO WHOEVER YOU MAY THINK INTERESTED. -- Posted: July 4th 2018 One PhD Student Position in Information and Communication Technologies on the research project "Quantum Annealing for SAT Solving (QUASI)" is available at the International Doctorate School in Information and Communication Technologies (http://www.ict.unitn.it/) of the University of Trento, Italy, under the supervision of Prof. Roberto Sebastiani, DISI, University of Trento, sponsored by and in direct collaboration with D-Wave Systems Inc. (http://www.dwavesys.com). The goal of the QuaSI project is to investigate the usage of D-Wave's quantum annealers (QAs) to solve hard propositional satisfiability (SAT) problems --and related NP-Hard problems-- by exploiting quantum effects to cope with the inherent complexity of the problem. The proposed research is to develop effective and efficient encoding procedures from SAT to problems which fit into, and can be solved by, D-Wave's QAs. These procedures will be presumably based on Satisfiability Modulo theories, automated-reasoning and graph-manipulation techniques. The ultimate goal is to solve problems (e.g., from cryptanalysis) which are currently out of the reach of state-of-the-art SAT solvers). Ph.D. courses will start in Autumn 2018, and the thesis must be completed in three-four years. The selected student should be available for an internship (e.g. 3-month) at D-Wave, in Vancouver (CA). People enrolled in Ph.D. courses are expected to move to Trento, and will receive monetary support during the phases of their activity. CANDIDATE PROFILE The ideal candidate should have an MS or equivalent degree in computer science or engineering, mathematics or electronic engineering, and combine solid theoretical background (algorithms, logic) and excellent software development skills. NO BACKGROUND KNOWLEDGE IN QUANTUM PHYSICS IS REQUIRED. Background knowledge and/or previous experience is requested in at least one the following areas (in order of preference): - Satisfiability Modulo Theories (SMT) - Propositional Satisfiability (SAT) - Automated reasoning and Computational Logic - Constraint Solving and Optimization - Operational Research The candidate should be able to work in a collaborative environment, with a strong commitment to reaching research excellence and achieving assigned objectives. The position is subject to the acceptance of the assignment of the ownership of intellectual property to D-Wave Inc. of the research results. APPLICATIONS AND INQUIRIES Interested candidates should inquire for further information and/or apply by sending email to roberto.sebasti...@unitn.it, indicating "PHD on Quasi Project" in the subject. Applications should contain a statement of interest, with a Curriculum Vitae, and three reference persons. PDF format is strongly encouraged. Emails will be automatically processed and should have as subject the sentence: 'PHD ON QUASI PROJECT' (Emails not complying with the above format have high chances to be ignored.) Eventually they must apply to the international call of the ICT school of DISI (http://ict.unitn.it), which is expected to appear by the end of July 2018 (application deadline: end of August 2018). PROPONENT AND CONTACT PERSON Prof. ROBERTO SEBASTIANI Software Engineering & Formal Methods Research Program DISI, University of Trento, via Sommarive 14, I-38100 Povo, Trento, Italy mailto: roberto[dot]sebastiani[at]unitn[dot]it url: http://disi.unitn.it/rseba/ CV: http://disi.unitn.it/rseba/inglcurr.pdf ABOUT DISI AND UNIVERSITY OF TRENTO University of Trento (http://www.unitn.it/en) in the latest years has always been rated among the top-three small universities in Italy. DISI (http://disi.unitn.it) has been recognized among the top three ICT University Department in Italy. DISI currently consists of ~40 faculties, ~70 research staff and support people, ~20 postdocs and ~140 Doctoral students, plus administrative and technical staff. DISI covers all the different areas of information technology (computer science, telecommunications, and electronics) and their applications. ABOUT D-WAVE INC. D-Wave (www.dwavesys.com) is the world's only commercial supplier of quantum computers. D-Wave's systems are being used by some of the world's most advanced organizations and D-Wave is the leader in the development and delivery of quantum and hybrid quantum-classical computing systems and software. D-Wave's technology is focused on annealing-based quantum computing. LOCATION Trento is a lively town of about 100.000 inhabitants, located 130 km south of the border between Italy and
[TYPES/announce] Research Assistant / Associate in Discipline Approximate Arithmetic
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear Colleagues, Please see http://www.jobs.ac.uk/job/BLB308/research-assistant-associate-in-disciplined-approximate-arithmetic for a vacancy in my group for a member of research staff to work on approximate computing. I’d be grateful if you could help spread the word. Thanks, George -- Professor George A. Constantinides Royal Academy of Engineering / Imagination Technologies Research Chair Head, Circuits and Systems Group Professor of Digital Computation g.constantini...@imperial.ac.uk Administrator: Mrs W. Hsissen (w.hsis...@ic.ac.uk) +44 20 7594 6261
