[TYPES/announce] PhD position at Inria / Nantes Université (France)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We would like to invite applications for a 3 years fully-funded PhD position within the Gallinette (https://urldefense.com/v3/__https://gallinette.gitlabpages.inria.fr/website/members.html__;!!IBzWLUs!W8TE65X6j2fnH5aotS4jGSreOtrgNP2NXXVJMA4N0AbfxyjHGYwkg0dO7B3OY8ePB5JrvwZnkecd6n8maK7fAPBqgInOEhkMPa6JSIVf$ ) Inria research group at Nantes Université (France). The successful candidate will contribute to the Fresco (https://urldefense.com/v3/__https://fresco.gitlabpages.inria.fr/__;!!IBzWLUs!W8TE65X6j2fnH5aotS4jGSreOtrgNP2NXXVJMA4N0AbfxyjHGYwkg0dO7B3OY8ePB5JrvwZnkecd6n8maK7fAPBqgInOEhkMPchs8hNq$ ) ERC project, aiming at designing fast and reliable symbolic computations. This project involves topics in program verification as well as in formalized mathematics. The start date is ideally in autumn 2023, but later dates can be negotiated. The candidate is expected to hold a master level degree in Mathematics or Computer Science before starting the enrollment procedure. Relevant keywords: dependent type theory, homotopy type theory, parametricity, type classes, hierarchies of mathematical structures universal algebra. Supervision: Assia Mahboubi (https://urldefense.com/v3/__http://people.rennes.inria.fr/Assia.Mahboubi/__;!!IBzWLUs!W8TE65X6j2fnH5aotS4jGSreOtrgNP2NXXVJMA4N0AbfxyjHGYwkg0dO7B3OY8ePB5JrvwZnkecd6n8maK7fAPBqgInOEhkMPWFcUHpg$ ), in collaboration with Cyril Cohen(https://urldefense.com/v3/__https://perso.crans.org/cohen/__;!!IBzWLUs!W8TE65X6j2fnH5aotS4jGSreOtrgNP2NXXVJMA4N0AbfxyjHGYwkg0dO7B3OY8ePB5JrvwZnkecd6n8maK7fAPBqgInOEhkMPba_2_t5$ ) (Inria) ## Contact assia.mahbo...@inria.fr ## Local scientific environment Gallinette (https://urldefense.com/v3/__https://gallinette.gitlabpages.inria.fr/website/members.html__;!!IBzWLUs!W8TE65X6j2fnH5aotS4jGSreOtrgNP2NXXVJMA4N0AbfxyjHGYwkg0dO7B3OY8ePB5JrvwZnkecd6n8maK7fAPBqgInOEhkMPa6JSIVf$ ) is a large joint research group of Inria and of the Laboratory of Digital Science of Nantes (LS2N). Research interests of the team include theoretical and implementation aspects of dependent type theory, extensions of the Curry-Howard correspondence, formalized mathematics, etc. ##Salary About 2000 euros monthly gross salary, including health insurance and partial covering of transportation costs. ## Location Downtown science campus of Nantes Université. ## Environment Nantes is a vibrant city rich in history and culture, located on the estuary of the Loire, less than 60km away from gorgeous shores of the Atlantic cost and 2h away from the center of Paris by fast train. ## How to apply Contact assia.mahbo...@inria.fr before **March 31 2023** and attach: - a covering letter - a recent curriculum vitae - available transcripts (Bachelor and Master if applicable) - the contact information of two references
[TYPES/announce] PhD position at Inria Rennes
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The CELTIQUE team (https://team.inria.fr/celtique/) has a PhD position available on the definition of a rule format to specify formal semantics and derive certified static analyzers in Coq. To see details and to apply, please go to https://jobs.inria.fr/public/classic/en/offres/2018-00650 Do not hesitate to forward this email to any appropriate candidate or mailing list. Best regards, Alan Schmitt -- OpenPGP Key ID : 040D0A3B4ED2E5C7 Monthly Athmospheric CO₂, Mauna Loa Obs. 2018-03: 409.46, 2017-03: 407.18 signature.asc Description: PGP signature
[TYPES/announce] PhD Position at INRIA Grenoble, France
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The WAM research project at INRIA Grenoble Rhone-Alpes invites applications for one PhD position on developing an XQuery Programming Environment for the mobile devices. -- Theme -- In the recent years, huge amounts of information from various application domains are stored, exchanged, and presented using XML. In this context, the ability to safely, efficiently and uniformly query XML data on different platforms such as mobile devices on a variety of data sources becomes increasingly important. XQuery is the W3C standard for querying XML data. It is increasingly popular and one of the challenges in web software development today is to help achieving a good level of quality in terms of programming frameworks, code size and runtime performance. In particular, with the recent advances in document formats such as the advent of HTML5, SVG and other UI oriented formats together with the increasing interaction between browsers and remote services, a general purpose, uniform and reliable alternative to JavaScript can be played with languages such as XQuery. -- Topic -- The topic of this PhD thesis consists in designing and implementing a programming environment for XQuery that can offer the following features: - A type inference system for XQuery - A Static type checker for XQuery - Automatic code optimization and dead-code analysis Based on these features, other applications can be built to offer security features for data manipulation such as path-based access control policies. On the theoretical side, the proposed work consists in extending an existing logical framework for XML reasoning to the modeling and reasoning on node sequences. The foundations are based on newly developed formal programming language verification techniques [1,2], which are now mature enough to be introduced in the context of software development. The WAM project seeks to establish logical foundations and automated reasoning techniques with applications concerning, but not limited to, static analysis of programs manipulating XML documents, pointer and heap analysis, program verification. Information about previous relevant research is available online: http://wam.inrialpes.fr/web-solver/webinterface.html -- Required Skills -- Applicants should have interests in programming languages, type theory, and/or mathematical logic, with a concern in the intersection of theory and practice. Expertise in the following areas are particularly welcomed: - programming language and type theory - program analysis - formal methods - automated reasoning -- References -- [1] Efficient Static Analysis of XML Paths and Types. Pierre Geneves, Nabil Layaida and Alan Schmitt. PLDI'07. [2] Impact of XML Schema Evolution. Pierre Geneves, Nabil Layaida and Vincent Quint. TOIT'11. [3] XQuery in the browser. Ghislain Fourny, Donald Kossmann, Tim Kraska, Markus Pilman, and Daniela Florescu. SIGMOD '08. -- Keywords -- XQuery, static analysis, type system, security, mobile computing -- How to apply -- Please submit your application through the link below: http://www.inria.fr/institut/recrutement-metiers/offres/theses/campagne-2011/%28view%29/details.html?id=PGTFK026203F3VBQB6G68LONZLOV5=4509LG=FRResultsperpage=20nPostingID=5115nPostingTargetID=10138option=52sort=DESCnDepartmentID=28 Pierre Geneves www.pierresoft.com/pierre.geneves
