[TYPES/announce] Researcher Positions in HoTT
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Senior and Post-Doctoral Researchers in Homotopy Type Theory / Category Theory / Type Theory / Homotopy Theory Carnegie Mellon University / Philosophy Department The research group in Homotopy Type Theory at Carnegie Mellon University seeks both Senior and Post-Doctoral Researchers, without teaching duties, for one academic year. The Senior Researcher position would be suitable for a Visiting Professorship as a sabbatical leave from your home institution. The Post-Doctoral Researcher position includes a possibility of renewal. Both positions could begin as early as August 2017, or later. Candidates should have a PhD and research experience in a relevant area and a desire to collaborate with the existing research group, which consists of several faculty members, postdocs, and graduate students. Questions about these positions may be directed to Steve Awodey, awo...@cmu.edu. Candidates should submit a CV and a brief research statement to cmuphiloso...@andrew.cmu.edu. ** More Information: Please visit “Why Carnegie Mellon” to learn more about becoming part of an institution inspiring innovations that change the world. A listing of employee benefits is available at: http://www.cmu.edu/jobs/benefits-at-a-glance/index.html Department URL: https://www.cmu.edu/dietrich/philosophy/ Primary Location: United States-Pennsylvania-Pittsburgh Time Type: Full Time Minimum Education Level: Doctorate or equivalent Salary: According to Experience ** Carnegie Mellon University does not discriminate in admission, employment, or administration of its programs or activities on the basis of race, color, national origin, sex, handicap or disability, age, sexual orientation, gender identity, religion, creed, ancestry, belief, veteran status, or genetic information. Furthermore, Carnegie Mellon University does not discriminate and is required not to discriminate in violation of federal, state, or local laws or executive orders. **
[TYPES/announce] Basili Postdoctoral Fellowship Program
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Below is a call for applications to the Basili Postdoctoral Fellowship Program at UMD, which is intended for post-docs working in programming languages and software engineering. We welcome and encourage applicants form the TYPES list. Successful applicants would be able to work with the PLUM lab, lead by Mike Hicks, Jeff Foster, and David Van Horn, as well as the current Basili scholars: Niki Vazou and Thomas Gilray. https://www.cs.umd.edu/basili-postdoc ;; The University of Maryland (UMD) Computer Science Department has a long history of leading research in software engineering and programming languages. To help ensure its continuing success, the UMD Computer Science Department is proud to announce the 2nd call for nominations for the Victor Basili Postdoctoral Fellowship. The fellowship program seeks talented, highly-motivated, post-doctoral computer scientists to conduct research in the area of Applied Software Engineering and Programming Languages, broadly construed. The primary goal of this effort is to build research collaborations and capacity to solve a variety of problems in government and industry by using cutting-edge software engineering and programming languages research. Extending the scope of the software engineering and programming languages programs from their established roots, the new initiative will allow researchers to work with existing faculty sponsors 1/2 time, while also allowing them freedom to being building their own new areas of research. We believe that this fellowship is quite unique in providing a supportive atmosphere, but also according postdocs the freedom to evolve their own research. The program supports multiple two-year postdoctoral appointments each year for several years, allowing new researchers to begin their careers at UMD, perform cutting edge research in applied software engineering and programming languages, and expand our existing CS research community. Professor Emeritus Victor Basili has generously supplied the program’s initial funding. One of last year’s new Basili Fellows, Thomas Gilray (http://thomas.gilray.org) reflecting on this experiences as a Basili Fellow writes: "The Basili fellowship has given me the opportunity to join the fantastic PLUM lab and pursue my interests in a lively and engaging collaborative environment. The fellowship gives me enormous freedom, in an ideal supportive context, to pursue collaborations with students doing exciting work, continuations of my previous efforts, and entirely new lines of research, with autonomy not usually found in a traditional post-doc. The department has accommodated my interests to collaborate on grant writing and to teach a class. It has also been a unique opportunity for me to develop as a programming languages scholar around great people who can help me to broaden myself and reach my potential." If you are interested in applying to the Victor Basili Postdoctoral Fellowship, you can learn more here: https://www.cs.umd.edu/basili-postdoc Review of applications will begin upon receipt and continue until positions are filled. If you have any questions, you are welcome to send an email to basilifel...@cs.umd.edu.
[TYPES/announce] Postdoc position at MPI-SWS, Kaiserslautern, Germany
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Applications are invited for a full-time postdoctoral research position at the Max Planck Institute for Software Systems (MPI-SWS) based at Kaiserslautern, Germany, under the supervision of Maria Christakis (https://mariachris.github.io/). MPI-SWS offers an internationally renowned research community as well as a multicultural and open working environment. Maria has recently won the prestigious EAPLS Best Dissertation Award and is excited to continue her work on Practical Formal Methods with a talented and motivated postdoctoral researcher. The initial postdoc appointment is for two years, starting anytime after October 2017, with an option to extend to a third year (depending on performance). The position is relatively independent in that it is not tied to a specific project and there is considerable freedom to choose a research topic. Nevertheless, the postdoc is expected to collaborate closely with other researchers in the group. Thus, the main topics of interest are: - defect analysis of smart contracts - collaborative verification and testing - systematic testing of large programs - practical concurrency error detection The successful candidate will have a strong background in at least one of the following areas: - automatic test generation - software verification - static and/or dynamic program analysis - security Qualified candidates are encouraged to contact Maria directly by e-mail (maria AT mpi-sws DOT org), and in addition, submit a formal online application at: https://apply.mpi-sws.org/ The application consists of a CV, a research statement, and a list of referees. Application deadline: Friday, 14 July.
[TYPES/announce] Deadline extension may 15: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] TFP 2017 EXTENSION: Deadline extension until Monday, 15 May (anywhere on earth). We encourage anyone who wants to present their work at TFP in Canterbury, England this June to submit a 2-10 page abstract if time is too short to put together a full paper. - F I N A L C A L L F O R P A P E R S - TFP 2017 === 18th Symposium on Trends in Functional Programming 19-21 June, 2017 University of Kent, Canterbury https://www.cs.kent.ac.uk/events/tfp17/index.html The symposium on Trends in Functional Programming (TFP) is an international forum for researchers with interests in all aspects of functional programming, taking a broad view of current and future trends in the area. It aspires to be a lively environment for presenting the latest research results, and other contributions (see below). Authors of draft papers will be invited to submit revised papers based on the feedback receive at the symposium. A post-symposium refereeing process will then select a subset of these articles for formal publication. TFP 2017 will be the main event of a pair of functional programming events. TFP 2017 will be accompanied by the International Workshop on Trends in Functional Programming in Education (TFPIE), which will take place on 22 June. The TFP symposium is the heir of the successful series of Scottish Functional Programming Workshops. Previous TFP symposia were held in * Edinburgh (Scotland) in 2003; * Munich (Germany) in 2004; * Tallinn (Estonia) in 2005; * Nottingham (UK) in 2006; * New York (USA) in 2007; * Nijmegen (The Netherlands) in 2008; * Komarno (Slovakia) in 2009; * Oklahoma (USA) in 2010; * Madrid (Spain) in 2011; * St. Andrews (UK) in 2012; * Provo (Utah, USA) in 2013; * Soesterberg (The Netherlands) in 2014; * Inria Sophia-Antipolis (France) in 2015; * and Maryland (USA) in 2016. For further general information about TFP please see the TFP homepage. (http://www.tifp.org/). == SCOPE == The symposium recognizes that new trends may arise through various routes. As part of the Symposium's focus on trends we therefore identify the following five article categories. High-quality articles are solicited in any of these categories: Research Articles: leading-edge, previously unpublished research work Position Articles: on what new trends should or should not be Project Articles: descriptions of recently started new projects Evaluation Articles: what lessons can be drawn from a finished project Overview Articles: summarizing work with respect to a trendy subject Articles must be original and not simultaneously submitted for publication to any other forum. They may consider any aspect of functional programming: theoretical, implementation-oriented, or experience-oriented. Applications of functional programming techniques to other languages are also within the scope of the symposium. Topics suitable for the symposium include, but are not limited to: Functional programming and multicore/manycore computing Functional programming in the cloud High performance functional computing Extra-functional (behavioural) properties of functional programs Dependently typed functional programming Validation and verification of functional programs Debugging and profiling for functional languages Functional programming in different application areas: security, mobility, telecommunications applications, embedded systems, global computing, grids, etc. Interoperability with imperative programming languages Novel memory management techniques Program analysis and transformation techniques Empirical performance studies Abstract/virtual machines and compilers for functional languages (Embedded) domain specific languages New implementation strategies Any new emerging trend in the functional programming area If you are in doubt on whether your article is within the scope of TFP, please contact the TFP 2017 program chairs, Scott Owens and Meng Wang. == BEST PAPER AWARDS == To reward excellent contributions, TFP awards a prize for the best paper accepted for the formal proceedings. TFP traditionally pays special attention to research students, acknowledging that students are almost by definition part of new subject trends. A student paper is one for which the authors state that the paper is mainly the work of students, the students are listed as first authors, and a student would present the paper. A prize for the best student paper is awarded each year. In both cases, it is the PC of
[TYPES/announce] PrePost 2017 CFP
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] First call for papers PrePost (Pre- and Post-Deployment Verification Techniques) Second International Workshop (Affiliated with iFM 2017, Torino, IT) http://staff.um.edu.mt/afra1/prepost17/ Scope The workshop aims to bring together researchers working in the field of computer-aided validation, programming languages and verification to discuss the connections and interplay between pre- and post-deployment verification techniques. Examples of the topics covered by the workshop are the relationships between classic model checking and testing on the one hand and runtime verification and statistical model checking on the other, and between type systems that may be checked either statically or dynamically through techniques such as runtime monitoring, gradual typing and contracts. Relevant topics also include the synthesis of runtime adaptation and enforcement mechanisms from correctness specifications, as well as the combination of deductive verification with runtime verification. Contributions related to tools and applications of pre- and post-deployment verification will also be welcome. Important Dates Abstract submission: June 5, 2017 Paper submission: June 12, 2017 Notification of acceptance:July 10, 2017 Camera ready version: July 17, 2017 Conference iFM 2017: Sep 20-22, 2016 Workshop PrePost 2017: Sep 19, 2017 Topics of Interest PrePost welcomes papers of either theoretical or applied interest, including case studies or experience reports dealing with the interplay between any of the pre- and post-verification techniques including: Monitoring, Enforcement and Adaptation Dynamic/Static/Gradual Type Systems Runtime Verification Model Checking Testing Program and Specification Logics Deductive Verification Submission We solicit the submission of original and unpublished contributions not under review for publication elsewhere. Contributions are expected to comprise research papers (with novel, previously unpublished results), experience reports of real-world applications, tool descriptions, as well as work-in-progress or exploratory ideas. All papers must be prepared in LaTeX using the EPTCS style. Full papers should not exceed 15 pages (typeset 11 points). Short papers should not exceed 8 pages. Additional details omitted due to space limitations may be included in a clearly marked appendix. Submissions must describe work unpublished in refereed venues, not submitted elsewhere. Contributions should be submitted in PDF format through the EasyChair online submission system: https://easychair.org/conferences/?conf=prepost17 Submission of a paper involves a firm commitment that at least one of the authors will attend and participate in the workshop in case the paper is accepted. Publication All contributions will be evaluated by at least three reviewers, chosen by the Program Committee. The PC will select the best papers based on their quality, relevance to the workshop, and potential to instigate discussion. All accepted papers will be included in the workshop proceedings, which will be published as a volume of the EPTCS series. We are looking into publishing selected papers in a special issue of a journal, following the standard reviewing process of the selected journal. Invited Speakers Luca Padovani (Università di Torino) Alex Mifsud (Ixaris Ltd.) Program Committee Laura Bocchi(University of Kent, UK) Dilian Gurov(KTH Royal Institute of Technology, Sweden) Adrian Francalanza (University of Malta, Chair) Heiko Mantel (TU Darmstadt, Germany) Leonardo Mariani (University of Milan Bicocca) Fabrizio Montesi(University of Southern Denmark, Denmark) Gordon J. Pace(University of Malta, Chair) Giles Reger (University of Manchester, UK) Kostis Sagonas (Uppsala University, Sweden) Cesar Sanchez (IMDEA Software Institute, Spain) Gerardo Schneider(Chalmers University of Technology, University of Gothenburg, Sweden) Yannis Smaragdakis(University of Massachusetts Amherst , US) Emilio Tuosto (University of Leicester, UK)
[TYPES/announce] AFM 2017 call for registration
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Registration is open for AFM 2017 (http://fm.csl.sri.com/AFM17). AFM has a workshop on May 19 at SRI International, and a day of tutorials on May 20 at Menlo College. The cost of registration is $50 a day (+ 3% for credit card payments). Note that we do not have hotel arrangements. Breakfast, lunch, and breaks are included. Payment will be accepted at the meetings. The sixth Automated Formal Methods (AFM) workshop will be held during May 19-20, 2017, at SRI International and Menlo College in Menlo Park. The earlier workshops were AFM06, AFM07, AFM08, AFM09, and AFM10. The 2017 workshop immediately follows the NASA Formal Methods (NFM) 2017 symposium. It consists of both invited talks and contributed papers on May 19, and tutorials covering recent progress in tools such as PVS, SAL/SALLY/HybridSAL, Yices, SeaHorn, Radler, and Bixie. AFM functions both as a user's meeting for SRI's tools such as PVS, SAL, and Yices, and as a workshop for those interested in state of the art automation for formal methods generally. Workshop Description AFM is a workshop centered around the use and integration of highly automated formal verification tools for specification, interactive theorem proving, satisfiability (SAT) and satisfiability modulo theories (SMT), model checking, program verification, static analysis, runtime verification, code generation, and testing, as well as interfaces, documentation, and education. This workshop was originally initiated as a users' group meeting for the SRI formal verification tools, which now include PVS, SAL, HybridSAL, SALLY, Yices, NL-Yices, Joogie, Bixie, and SeaHorn, together with technologies under development, such as ARSENAL, Radler, Occam, PCE, and ETB. However, topics are not restricted to these tools: we welcome contributions on all aspects of state of the art automation. The proceedings of the workshop will be published through the ACM Digital Library. Workshop Program The program includes contributed papers and invited talks selected by the international program committee on May 19, and a series of tutorials on May 20, 2017. Program Committee Saddek Bensalem (Verimag) Matthew Bolton (Buffalo) Maria Paola Bonacina (Verona) Alessandro Coglio (Kestrel Institute) Bruno Dutertre (SRI, co-Chair) Leonard Gerard (SRI) Stephane Graham-Lengrand (Ecole Polytechnique) Arie Gurfinkel (U. of Waterloo) Liana Hadarean (Synopsys) Ben Hocking (Dependable Computing) Susmit Jha (SRI) Dejan Jovanovic (SRI) Temesghen Kahsai (CMU West) Aditya Kanade (IISc, Bangalore) Wenchao Li (Boston University) Paolo Masci (Queen Mary) Mariano Moscato (NIA) Cesar Munoz (NASA Langley) Anitha Murugesan (Honeywell Research) Jorge Navas (SRI) Natasha Neogi (NIA) Sam Owre (SRI) Lee Pike (Galois) Elvinia Riccobene (Milan) Kristin Rozier (Iowa) John Rushby (SRI) Martin Schaef (SRI) Natarajan Shankar (SRI, co-Chair) Wilfried Steiner (TTTech) Ashish Tiwari (SRI) Alan Wassyng (McMaster University)
[TYPES/announce] CAV 2017: Call for participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] ** CALL FOR PARTICIPATION Computer-Aided Verification, 29th International Conference CAV 2017 Heidelberg, Germany, 22-28 July 2017 http://www.cavconference.org/2017 ** TL;DR Early registration: June 14, 2017; Hotel booking deadlines: early June, 2017 We hope to welcome you at CAV -- we have an exciting program! -- ABOUT CAV -- CAV 2017 is the 29th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. Along with the main conference, CAV will feature eight workshops (including a special workshop in honor of David Dill) and tutorials. Highlights: -- WORKSHOPS (22-23 July) -- VERIFICATION MENTORING WORKSHOP (23 July) -- SPECIAL WORKSHOP Dill@60 in Honor of David Dill (24 July) -- MAIN CONFERENCE (24-28 July) -- INVITED SPEAKERS -- * Chris Hawblitzel, Microsoft Research * Marta Kwiatkowska, Oxford * Viktor Vafeiadis, MPI-SWS * Winner of the CAV award (to be announced at the conference) -- INVITED TUTORIALS * Loris D’Antoni, University of Wisconsin-Madison: The power of symbolic automata and transducers * Mayur Naik, University of Pennsylvania: Maximum Satisfiability in Software Analysis: Applications and Techniques -- PUBLIC LECTURE ``Logic Lounge'' in memory of Helmut Veith * Fabiana Zollo: Social Dynamics in the Post-Truth Society: How the Confirmation Bias is Changing the Public Discourse -- CONTRIBUTED PAPERS -- See the list of accepted papers at the conference website. -- SATELLITE EVENTS (22-23 July) -- 7 satellite workshops will take place before CAV 2017. Check their calls for papers and consider contributing! • SYNT – Sixth Workshop on Synthesis (July 22) • DARS – Design and Analysis of Robust Systems (July 22) • NSV/Rise4CPS – Numerical Software Verification and Formal Methods for Rigorous Systems Engineering of Cyber-Physical Systems (July 22-23) • SMT – Satisfiability Modulo Theories (July 22-23) • VSTTE – Verified Software: Theories, Tools, and Experiment (July 22-23) • VMW – Verification Mentoring Workshop (July 23) • FEVER – Formal Approaches to Explainable VERification (July 23) -- REGISTRATION -- Early registration is until Wednesday, June 14, 2017 (AOE). http://cavconference.org/2017/registration/ -- VENUE -- Workshops will be organized at the Crowne Plaza hotel in Heidelberg City Center. The conference will be organized at the beautiful Heidelberg Stadthalle by the River Neckar. -- ACCOMMODATION -- The organizers have negotiated special rates from several hotels in Heidelberg. To benefit from those, follow the instructions on the conference website. The offers expire on different dates on or before the early registration deadline. Heidelberg is a busy tourist destination in July. It is important to book your hotel as soon as possible! -- HOST CITY -- Heidelberg is a picturesque city one the river Neckar at the heart of the 'Rhine-Neckar Triangle' in western Germany. It is renowned for its medieval castle, its old university (founded in 1386) and "Philosopher's Walk," and its historic old town. It is a cosmopolitan and vibrant college town with a rich academic and cultural tradition (including a 16th century Student Jail for mischievous students :-o). https://en.wikipedia.org/wiki/Heidelberg July is warm and sunny for the most part. It is also high tourist season. -- ORGANIZERS -- We hope to welcome you to CAV 2017! Viktor Kuncak (EPFL) Rupak Majumdar (MPI-SWS)
[TYPES/announce] Second CFP: ML Family Workshop 2017
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] -- CALL FOR PAPERS ML Family Workshop 2017 7 September 2017, Oxford, UK http://www.mlworkshop.org/ml2017/ (co-located with ICFP) -- ML is a family of programming languages that includes Standard ML, OCaml, F#, SML#, Manticore, MetaOCaml, JoCaml, Alice ML, Dependent ML, Flow Caml, and many others. All ML languages share several fundamental traits, besides a good deal of syntax. They are higher-order, strict, mostly pure, and typed, with algebraic and other data types. Their type systems are derived from Hindley-Milner. The development of these languages has inspired a significant body of computer science research and influenced the design of many other programming languages, including Haskell, Rust, and Scala. ML workshops have been held in affiliation with ICFP continuously since 2005. This workshop specifically aims to recognise the entire extended ML family and to provide a forum for presenting and discussing common issues, both practical (compilation techniques, implementations of concurrency and parallelism, programming for the Web) and theoretical (fancy types, module systems, metaprogramming). The scope of the workshop includes all aspects of the design, semantics, theory, application, implementation, and teaching of the members of the ML family. We also encourage presentations from related languages (such as ATS, Eff, F*, Koka, Links, Rust, Scala, Swift, etc.), to exchange experience of further developing ML ideas. Last year's ML Family workshop included talks covering eight different ML dialects and related languages: Eff, F#, F*, Links, Manticore, OCaml, SML, and SML#. The ML family workshop will be held in close coordination with the OCaml Users and Developers Workshop. Invited speaker --- Edwin Brady (University of St Andrews, UK) Scope - We acknowledge the whole breadth of the ML family and aim to include languages that are closely related, such as Rust and Scala. Those languages have implemented and investigated run-time and type system choices that may be worth considering for OCaml, F# and other ML languages. We also hope that the exposure to state of the art ML might favourably influence those related languages. Specifically, we seek research presentations on topics including (but not limited to): * Language design: abstraction, higher forms of polymorphism, concurrency, distribution and mobility, staging, extensions for semi-structured data, generic programming, object systems, etc. * Implementation: compilers, interpreters, type checkers, partial evaluators, runtime systems, garbage collectors, foreign function interfaces, etc. * Type systems: inference, effects, modules, contracts, specifications and assertions, dynamic typing, error reporting, etc. * Applications: case studies, experience reports, pearls, etc. * Environments: libraries, tools, editors, debuggers, cross-language interoperability, functional data structures, etc. * Semantics: operational and denotational semantics, program equivalence, parametricity, mechanization, etc. Four kinds of submissions will be accepted: Research Presentations, Experience Reports, Demos and Informed Positions. * Research Presentations: Research presentations should describe new ideas, experimental results, or significant advances in ML-related projects. We especially encourage presentations that describe work in progress, that outline a future research agenda, or that encourage lively discussion. These presentations should be structured in a way which can be, at least in part, of interest to (advanced) users. * Experience Reports: Users are invited to submit Experience Reports about their use of ML and related languages. These presentations do not need to contain original research but they should tell an interesting story to researchers or other advanced users, such as an innovative or unexpected use of advanced features or a description of the challenges they are facing or attempting to solve. * Demos: Live demonstrations or short tutorials should show new developments, interesting prototypes, or work in progress, in the form of tools, libraries, or applications built on or related to ML and related languages. (You will need to provide all the hardware and software required for your demo; the workshop organisers are only able to provide a projector.) * Informed Positions: A justified argument for or against a language feature. The argument must be substantiated, either theoretically (e.g. by a demonstration of (un)soundness, an inference
