[TYPES/announce] Postdoctoral researcher: opening at the University of Cambridge
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We have an opening at the University of Cambridge for a postdoctoral researcher on the Modular Macros <https://urldefense.com/v3/__https://www.cl.cam.ac.uk/*jdy22/projects/modular-macros/__;fg!!IBzWLUs!GGG2mZx7DnS32kq_n0gkei2Sk6I7SHEyYH5Jf16e8lp-jk46ADeWHQ-r5u8arLxAlkE-FmQJWeGhWw$ > project, which extends OCaml with new language features for typed compile-time computation. More details and an application form can be found here: https://urldefense.com/v3/__https://www.jobs.cam.ac.uk/job/34041/__;!!IBzWLUs!GGG2mZx7DnS32kq_n0gkei2Sk6I7SHEyYH5Jf16e8lp-jk46ADeWHQ-r5u8arLxAlkE-FmSYZC6xFA$ Applications are invited for a Research Assistant/Associate to join the Modular Macros project. The Modular Macros project brings new language features for typed, hygienic, compile-time computation to OCaml, making it possible for programmers to write high-level abstract libraries that generate efficient low-level code. Our design builds on a long tradition of work in multi-stage programming, taking inspiration from languages such as MetaML, MetaOCaml and Typed Template Haskell, and integrating smoothly with existing OCaml features, such as its advanced module system. We'll port existing multi-staged libraries and develop new applications that combine high-level abstractions with outstanding performance. The position will involve working with Modular Macros project members at the University of Cambridge and industrial partners including Jane Street Capital to develop, formalise and implement the design of Modular Macros. The successful candidate is likely to have (or expect to be awarded soon) a PhD in computer science or a related discipline, as well as a track record of published research and experience or demonstrable interest in some combination of the following: - Programming language design and formalisation - Implementation of programming languages, broadly construed (including compilers, interpreters, proof assistants, static analysers and language tools) Informal enquiries are welcome and should be directed to Dr Jeremy Yallop (jeremy.yal...@cl.cam.ac.uk)
[TYPES/announce] Postdoctoral Position at the University of Cambridge
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Posting on behalf of Neel Krishnaswami] Hello, We have an opening in Cambridge for a postdoctoral position with the ERC Consolidator Grant project TypeFoundry. The TypeFoundry project aims to use recent developments in proof theory and semantics, such as polarized type theory and call-by-push-value, to identify the theoretical structures underpinning bidirectional type inference. Informal enquiries are welcome and should be directed to Dr Neel Krishnaswami (nk...@cl.cam.ac.uk). More details and an application form can be found at < https://www.jobs.cam.ac.uk/job/30485/>. - Research Associate: £32,816 -£40,322 Fixed-term: The funds for this post are available for 2 years in the first instance with the possibility of extension. We invite applications for a Postdoctoral Research Associate to join the TypeFoundry project. The TypeFoundry project aims to use recent developments in proof theory and semantics, such as polarized type theory and call-by-push-value, to identify the theoretical structure underpinning bidirectional type inference. The overall aim is to develop a theory of type inference capable of scaling up to the support both the wide variety of advanced type system features language designers are interested in (ranging from languages based on substructural types like Rust to dependent type theories like Agda or Idris), and with a framework for proof which scales beyond kernel calculi all the way up to full-scale languages. The project will focus on developing and proving the correctness of new bidirectional type inference algorithms; identifying the common categorical/algebraic structure which makes these algorithms work; and using that structure to develop tooling which can automate the generation of type inference algorithms, as well as support mechanised proofs of their correctness. The position will involve working with TypeFoundry project members (including both PhD students and faculty). It will run initially for 24 months, with the possibility for a further 12 month extension,on any aspect of this project. The successful candidate is likely to have (or expect to be awarded soon) a PhD in computer science or related discipline, as well as a track record of research expertise in a subset of the following topics: Type inference and type theory Structural proof theory Categorical semantics of programming languages Functional programming language implementation Use of dependent type theories and proof assistants (eg, Coq or Agda) Informal enquiries are welcome and should be directed to Dr Neel Krishnaswami (nk...@cl.cam.ac.uk). The University of Cambridge is committed in its pursuit of academic excellence to a proactive and inclusive approach to equality, which supports and encourages all under-represented groups, promotes an inclusive culture, and values diversity.
[TYPES/announce] Postdoc position at Cambridge in programming with equations
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We have an opening in Cambridge for a researcher on the Frex project (https://www.cl.cam.ac.uk/~jdy22/projects/frex). Informal enquiries are welcome: please feel free to get in touch. --- Research Assistant / Associate in Programming with Equations (Fixed Term) https://www.jobs.cam.ac.uk/job/29773/ Applications are invited for a Research Assistant/Associate to join the Frex project. The Frex project investigates the use of equations in programming. There is often a large gap between what programmers know about their programs and what compilers are able to deduce. Frex targets this gap by exposing to the compiler the equations proved by programmers about programs so that they can be used to improve optimisation and type checking. The position will involve working with Frex project members at the Universities of Cambridge, Edinburgh and St Andrews to extend and improve the design and implementations of Frex. Work up to this point has focused on equations for first-order single-sorted algebras and we plan to extend the techniques to more elaborate settings. The successful candidate is likely to have (or expect to be awarded soon) a PhD in computer science or a related discipline, as well as a track record of published research and experience or demonstrable interest in some combination of the following: - Dependently typed programming languages or proof assistants based on type theory (e.g. Agda, Idris, Coq, Lean) - Functional programming languages (e.g. F#, OCaml, Haskell) - Partial evaluation, normalization by evaluation, multi-stage programming, supercompilation or related techniques - Algebraic structures, universal algebra and categorical algebra Informal enquiries are welcome and should be directed to Dr Jeremy Yallop (jeremy.yal...@cl.cam.ac.uk) Expected starting date: 1 September 2021
[TYPES/announce] Metaprogramming Summer School (August 2019): call for applications
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Second International Summer School on Metaprogramming Schloss Dagstuhl, Leibniz Center for Informatics, Germany 11th-16th August 2019 (the week before ICFP'19) https://www.cl.cam.ac.uk/events/metaprog/2019/ Metaprogramming is an approach to constructing programs by treating program fragments (such as expressions or types) as values that the program can manipulate. Metaprogramming comes in various forms --- for example, * in dependently-typed programming terms appear within types, supporting the construction of precise specifications of functions and data. * in multi-stage programming expressions are program values, making it possible to write safe program generation programs that can significantly improve performance. * in languages with macros programs execute partly during compilation and partly at run-time, eliminating the sharp distinction between built-in and user-defined constructs. * embedded domain-specific languages reuse host language features such as syntax and type-checking for convenient definition of little languages suited to a particular endeavour. Metaprogramming has many applications, including genericity, proof automation, language extensibility and user-defined optimization. The goal of the summer school is to explore the state-of-the art in metaprogramming and its applications, covering both theory and practice. Lecturers and courses Oleg Kiselyov (Tohoku University) From the tagless-final cookbook: simple hardware description language and optimization-by-evaluation Matthew Flatt (University of Utah) Building Languages with Racket Conor McBride (University of Strathclyde) TBD Jonathan Protzenko (Microsoft Research Redmond) Meta-F*: efficient meta-programming of the F* compiler at every stage Prerequisites The school is aimed at graduate students in programming languages and related areas, but is open to researchers, practitioners and strong masters students with the support of a supervisor. Some experience of typed functional programming in Haskell, OCaml, Scala, or a similar language will be assumed. Costs Thanks to the Schloss Dagstuhl subsidies, accommodation costs are as follows, and the dates are immediately before ICFP'19 (also in Germany): Single-occupancy accommodation: €420 Double-occupancy accommodation: €330 Accommodation costs include full board (in a single- or double-occupancy room, including meals during stay) from Sunday 11 August (evening) to Friday 16 August (afternoon). Application procedure You will need to complete the online registration form at: https://www.cl.cam.ac.uk/events/metaprog/2019/application.html and ensure your referees send your references to: metaprog-2...@cl.cam.ac.uk by the application deadline. TIMETABLE * 30 June: Application and reference letters deadline. * 10 July: Notification of acceptance. * 11 August: Summer school. Further information For any questions relating to the school, please contact the organisers (Jeremy Yallop, Ohad Kammar, Yukiyoshi Kameyama) at metaprog-2...@cl.cam.ac.uk
[TYPES/announce] Partial Evaluation & Program Manipulation (PEPM'17): Call for Participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] CALL FOR PARTICIPATION Workshop on PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM 2017) http://conf.researchr.org/home/PEPM-2017 Paris, France, January 16th - 17th, 2017 (co-located with POPL 2017) Registration http://popl17.sigplan.org/attending/registration Early registration deadline: Saturday 17th Dec 2016 Programme - Monday 16th January 09:00-10:00: Keynote Compiling Untyped Lambda Calculus to Lower-Level Code by Game Semantics and Partial Evaluation Neil D. Jones (with Daniil Berezun) 10:30-12:00: Programming languages Lightweight Soundness for Towers of Language Extensions Alejandro Serrano, Jurriaan Hage Detecting code clones with gaps by function applications Tsubasa Matsushita, Isao Sasano PEG Parsing in Less Space Using Progressive Tabling and Dynamic Analysis Fritz Henglein, Ulrik Terp Rasmussen 14:00-15:30: Tutorial and Poster Session Idris, Inside-Out: A Tutorial on Extending Idris in Idris David Christiansen Language-integrated Query with Ordering, Grouping and Outer Joins (poster) Tatsuya Katsushima, Oleg Kiselyov 16:00-17:00: Transformation (part I) Verification of Code Generators via Higher-Order Model Checking Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi Interactive data representation migration: Exploiting program dependence to aid program transformation Krishna Narasimhan, Julia Lawall, Christoph Reichenbach Tue 17th January 09:00-10:00: Tutorial Reversible computing from a programming language perspective Robert Glück 10:30-12:00: Types Cost versus Precision for Approximate Typing for Python Levin Fritz, Jurriaan Hage Refining types using type guards in TypeScript Ivo Gabe de Wolff, Jurriaan Hage Predicting Resource Consumption of Higher-Order Workflows Markus Klinik, Jurriaan Hage, Jan Martin Jansen, Rinus Plasmeijer 14:00-15:30: Tutorial Practical Partial Evaluation for Language Implementation with Graal & Truffle Gilles Duboscq 16:00-17:00: Transformation (part II) Functional Parallels of Sequential Imperatives Tiark Rompf, Kevin J. Brown A Functional Reformulation of UnCAL Graph-Transformations: Or, Graph Transformation as Graph Reduction Kazutaka Matsuda, Kazuyuki Asada
[TYPES/announce] PEPM 2017 Final Call for Papers (submission deadline extension: 30th Sep.)
outside of North America and Europe. For details on the PAC programme, see its web page. Publication and special issue - All accepted papers, short papers and posters included, will appear in formal proceedings published by ACM Press. Accepted papers will be included in the ACM Digital Library. Authors of selected papers from PEPM 2016 and PEPM 2017 will also be invited to expand their papers for publication in a special issue of the journal Computer Languages, Systems and Structures (COMLAN, Elsevier). Keynote --- Neil Jones (DIKU) will give the PEPM keynote talk, titled Compiling Untyped Lambda Calculus to Lower-level Code by Game Semantics and Partial Evaluation Best paper award PEPM 2017 continues the tradition of a Best Paper award. The winner will be announced at the workshop. Submission -- Papers should be submitted electronically via HotCRP. https://pepm17.hotcrp.com/ Authors using LaTeX to prepare their submissions should use the new improved SIGPLAN proceedings style, and specifically the sigplanconf.cls 9pt template. Important Dates --- UPDATE: following feedback from potential authors, we have extended the PEPM submission dates by two weeks to avoid clashes with other events. The new deadlines are consequently strict, and there will be no further extensions. For Regular Research Papers and Short Papers: * Abstract submission : Tuesday 27th September 2016 * Paper submission: Friday 30th September 2016 * Author notification : Friday 4th November 2016 * Camera ready: Monday 28th November 2016 For Posters: * Poster submission : Tuesday 8th November 2016 * Author notification : Friday 18th November 2016 * Camera ready: Monday 28th November 2016 PEPM workshop: * Workshop: Monday 16th - Tuesday 17th January 2017 The proceedings will be published 2 weeks pre-conference. AUTHORS TAKE NOTE: The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of your conference. The official publication date affects the deadline for any patent filings related to published work. (For those rare conferences whose proceedings are published in the ACM Digital Library after the conference is over, the official publication date remains the first day of the conference.). PEPM'17 Programme Committee --- Elvira Albert (Complutense University of Madrid, Spain) Don Batory (University of Texas at Austin, USA) Martin Berger (University of Sussex, UK) Sebastian Erdweg (TU Delft, Netherlands) Andrew Farmer (Facebook, USA) Matthew Flatt (University of Utah, USA) John Gallagher (Roskilde University, Denmark) Robert Glück (DIKU, Denmark) Jurriaan Hage (Utrecht University, Netherlands) Zhenjiang Hu (National Institute of Informatics, Japan) Yukiyoshi Kameyama (University of Tsukuba, Japan) Ilya Klyuchnikov (Facebook, UK) Huiqing Li (EE, UK) Annie Liu (Stony Brook University, USA) Markus Püschel (ETH Zurich, Switzerland) Ryosuke SATO (University of Tokyo, Japan) Sven-Bodo Scholz (Heriot-Watt University, UK) Ulrik Schultz (co-chair) (University of Southern Denmark) Ilya Sergey (University College London, UK) Chung-chieh Shan (Indiana University, USA) Tijs van der Storm (Centrum Wiskunde & Informatica, Netherlands) Jeremy Yallop (co-chair) (University of Cambridge, UK)
[TYPES/announce] International summer school on metaprogramming (Cambridge, 8-12 Aug 2016)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] International summer school on metaprogramming Robinson College, Cambridge, United Kingdom 8th-12th August, 2016 http://www.cl.cam.ac.uk/events/metaprog2016/ Metaprogramming is an approach to improving programs by treating program fragments (such as expressions or types) as values that the program can manipulate. Metaprogramming comes in various forms, including * staged programming: treating expressions as program values. The execution of a staged program is spread over several phases, with each stage using the available data to generate specialized code. Staged programming has a wide variety of applications — numeric computations, parsing, database queries, generic programming, domain specific languages, and many more. Precompiling the staged code can have dramatic performance improvements, in some cases an order of magnitude or more. * generic programming: treating types as program values. Generic programming can improve code flexibility, allowing to give a single definition of a function that operates in a predictable (but not uniform) way on many different types. Generic programming techniques can be used to define a wide variety of functions, including traversals, comparisons, pretty printers, serialization functions, and many more. The goal of the summer school is to explore the state-of-the art in metaprogramming and its applications, covering both theory and practice. Lecturers and courses Philip Wadler, Sam Lindley and Shayan Najd (University of Edinburgh) Normalisation and embedding Simon Peyton Jones (Microsoft Research) Oleg Kiselyov (Tohoku University) Type-safe embedding and optimizing domain-specific languages in the typed final style Laurence Tratt (Kings College London) The highs and lows of macros in a modern language Jeremy Yallop (University of Cambridge) Staging generic programming Martin Berger (University of Sussex) Foundations of meta-programming José Pedro Magalhães (Standard Chartered) Prerequisites The school is aimed at graduate students in programming languages and related areas, but is open to researchers, practitioners and strong masters students with the support of a supervisor. Some experience of typed functional programming in Haskell, OCaml, Scala, or a similar language will be assumed. Costs Thanks to generous industrial sponsorship, we are able to offer places with significantly reduced fees. There are three categories of fees, all of which cover registration, accommodation in Robinson College from Monday to Friday, and all meals and refreshments. Participants who can pay the full fees will help allocate more fully-subsidised slots to less financially-able students. Your category of fees will not have any direct bearing on your acceptance into the school, but could affect how many slots we can offer. * The full fee is £800. * The standard (partly-subsidised) fee is £295. * We also have a limited number of fully-subsidised places available for a nominal registration fee of £50. We will notify you of your fee upon acceptance. Application procedure You will need to complete the online registration form at: http://www.cl.cam.ac.uk/events/metaprog2016/application.html and ensure your referees send your references to: metaprog-2...@cl.cam.ac.uk by the application deadline. TIMETABLE * 30 June: Application and reference letters deadline. * 10 July: Notification of acceptance. * 24 July: Registration deadline. * 8 August: Summer school. Further information For questions relating to the material of the school, please contact Jeremy Yallop (jeremy.yal...@cl.cam.ac.uk) Ohad Kammar (ohad.kam...@cs.ox.ac.uk) For administrative questions, please contact Gemma Gordon (gg...@cl.cam.ac.uk)
[TYPES/announce] Call for participation: ML 2015
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Higher-order, Typed, Inferred, Strict: ACM SIGPLAN ML Family Workshop Thursday 3 September 2015, Vancouver, Canada (co-located with ICFP) Call For Participation:http://www.mlworkshop.org/ml2015/ Early registration deadline: Monday 3 August 2015 Register online: https://regmaster4.com/2015conf/ICFP15/register.php The ML Family Workshop brings together researchers, implementors and users of languages in the extended ML family and provides a forum to present and discuss common issues, both practical (compilation techniques, tooling, embedded programming) and theoretical (fancy types, module systems, type inference). ML 2015 will be held in Vancouver on 3 September, immediately after ICFP and close to a number of other related events, including the OCaml Workshop on the following day. Programme (Talk times and abstracts are available from the workshop website: http://www.mlworkshop.org/ml2015/). * The History of Standard ML: Ideas, Principles, Culture (Invited Talk) David MacQueen * Generating code with polymorphic let Oleg Kiselyov * Polymorphism, subtyping and type inference in MLsub Stephen Dolan and Alan Mycroft * Arduino programming of ML-style in ATS Kiwamu Okabe and Hongwei Xi * Resource monitoring for Poly/ML processes David Matthews, Magnus Stenqvist and Tjark Weber * Full dependency and user-defined effects in F* Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Pierre-Yves Strub, Aseem Rastogi, Antoine Delignat-Lavaud, Karthikeyan Bhargavan, and Cédric Fournet * Dependent types for real-time constraints William Blair and Hongwei Xi * Manifest contracts for OCaml Yuki Nishida and Atsushi Igarashi * Lost in extraction, recovered Éric Tanter and Nicolas Tabareau * GADTs and exhaustiveness: looking for the impossible Jacques Garrigue and Jacques Le Normand Programme Committee Damien Doligez (Inria Paris-Rocquencourt, France) Suresh Jagannathan (Purdue University, USA) Patricia Johann (Appalachian State University, USA) Sam Lindley (University of Edinburgh, UK) Moe Masuko (Ochanomizu University, Japan) Adriaan Moors (Typesafe, USA) Scott Owens (University of Kent, UK) Jonathan Protzenko (Microsoft Research, USA) Martin Sulzmann (Karlsruhe University of Applied Sciences, Germany) Jeremy Yallop (University of Cambridge, UK) (PC chair)
[TYPES/announce] CFP: ML 2015
. There are no published proceedings, so contributions may be submitted for publication elsewhere. We hope that this format will encourage the presentation of exciting (if unpolished) research and deliver a lively workshop atmosphere. Each presentation should take 20-25 minutes, except demos, which should take 10-15 minutes. The exact time will be decided based on the number of accepted submissions. The presentations will likely be recorded. Post-proceedings ML 2015 is an informal workshop without proceedings. We are planning to publish a post-proceedings and to invite interested authors of selected presentations to expand their abstracts for inclusion. Coordination with the OCaml Users and Developers Workshop -- --- The OCaml workshop is seen as more practical and is dedicated in significant part to OCaml community building and the development of the OCaml system. In contrast, the ML family workshop is not focused on any language in particular, is more research-oriented, and deals with general issues of ML-style programming and type systems. Yet there is an overlap, which we are keen to explore in various ways. The authors who feel their submission fits both workshops are encouraged to mention it at submission time or contact the Programme Chairs. Submission details -- Submissions should be at most two pages, in PDF format, and printable on US Letter or A4 sized paper. A submission should have a synopsis (2-3 lines) and a body between 1 and 2 pages, in one- or two-column layout. The synopsis should be suitable for inclusion in the workshop programme. Submissions must be uploaded to the workshop submission website before the submission deadline (Monday 18th May, 2015). If you have a question concerning the scope of the workshop or the submission process, please contact the programme chair. Important dates --- Monday 18th May (any time zone) Abstract submission deadline Monday 29th June Author notification Thursday 3rd September 2015 ML Family Workshop Programme committee --- Damien Doligez (Inria Paris-Rocquencourt, France) Suresh Jagannathan (Purdue University, USA) Patricia Johann (Appalachian State University, USA) Sam Lindley (University of Edinburgh, UK) Moe Masuko (Ochanomizu University, Japan) Adriaan Moors (Typesafe, USA) Scott Owens (University of Kent, UK) Jonathan Protzenko (Microsoft Research, USA) Martin Sulzmann (Karlsruhe University of Applied Sciences, Germany) Jeremy Yallop (University of Cambridge, UK) (PC chair)
