Call for Papers Workshop on Logic Programming for Type Inference 16-17 October 2016, New York, USA https://ff32.host.cs.st-andrews.ac.uk/lpti16/
Objectives and scope ------------------- Two facts are universally acknowledged: critical software must be subject to formal verification and modern verification tools need to scale and become more user-friendly in order to make more impact in industry. There are two major styles of verification: algorithmic : verification problems are specified in an automated prover, e.g. (constraint) logic programming or SMT solver, and properties of interest are verified by the prover automatically. Such provers can be fast, but their trustworthiness is hard to establish without producing and checking proofs. An alternative is a typeful approach to verification: instead of verifying programs in an external prover, a programmer may record all properties of interest as types of functions in his programs. Thanks to Curry-Howard isomorphism, type inhabitants also play the role of runnable functions and proof witnesses, thus completing the certification cycle. At their strongest, types can cover most of the properties of interest to the verification community, e.g. recently proposed Liquid Haskell and F* allow pre- and post-condition formulation at type level. But, when properties expressed at type level become rich, type inference engines have to assume the role of automated provers, e.g. Liquid Haskell and F* connect directly to SMT solvers. The above trend of integrating automated theorem proving with types calls for more precise methods of automated proof certification and integration of automated provers with modern-day compilers. This workshop aims to identify challenges in type inference in various domains and facilitate the research communities to collaboratively seek for effective methods, primarily focusing on Logic Programming (LP), in a broad sense, which includes resolution-based systems, constraint solving, ATPs, and also ITPs with sufficient support for automation. The term "type inference" is also used in a broad sense including all three directions of type related computations: type checking, type inference, and type inhabitation. The topics of interests include but are not limited to: * deriving implementations and/or proofs from declarative specifications of type systems, * identifying challenges and/or introducing approaches on type inference for non-traditional type systems (e.g., gradual/hybrid typing, success typing, types for process calculus, ...), * innovative ideas and new/old theories of LP that could benefit type inference, * integration of LP methods within other parts of language systems and tools, and * adding/enhancing support for type inference in LP systems themselves. Venue and event --------------- LPTI will be held in New York, USA, on 16-17 October 2016, co-located with International Conference on Logic Programming, ICLP-2016. Invited speakers --------------- * Logic programming for type inference in object-oriented languages, Davide Ancona, University of Genoa, Italy * Automation of type inference in functional languages: Liquid Haskell, Niki Vazou, University of California, San Diego, USA * Type inference applications in industry, TBA Invited tutorial speakers ------------------------- * Horn Clauses as types: proof-relevant resolution for Haskell type classes, Peng Fu, Heriot-Watt University, UK * Relational Specification of type systems using LP, Ki Yung Ahn, Korea University, Sejong City, Korea Important dates --------------- Paper submission: 1 August, 2016 Notification to authors: 21 August, 2016 LPTI'16 Workshop: 16-17 October, 2016 Post-proceedings: 5 November, 2016 Programme committee ------------------- Ki Yung Ahn, Korea University, Sejong City, Korea Davide Ancona, University of Genoa, Italy Iavor Diatchki, Galois, Inc, USA Peng Fu, Heriot-Watt University, UK Patricia Johann, Appalachian State University, USA Ekaterina Komendantskaya, Heriot-Watt University, UK J. Garrett Morris, University of Edinburgh, UK Claudio Russo, Microsoft Research Cambridge, UK Stephan Schulz, DHBW Stuttgart, Germany Aaron Stump, The University of Iowa, USA Niki Vazou, University of California, San Diego, USA Joe Wells, Heriot-Watt University, UK Publicity chair --------------- FrantiĊĦek Farka, University of Dundee, UK and University of St Andrews, UK PC chair -------- Ekaterina Komendantskaya, Heriot-Watt University, UK Submission guidelines --------------------- Submissions must be made via EasyChair at https://easychair.org/conferences/?conf=lpti2016. We solicit two types of contributions: 1. Regular papers to be evaluated by the PC for publication in the proceedings: They must have a length of at most 20 pages, formatted in the EPTCS style. They must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. 2. Short contributions: These will not be published in the proceedings but will be bundled in a technical report. They should be no more than two pages in the EPTCS style and may describe work in progress, summarise work submitted to a conference or workshop elsewhere, or in some other way appeal to the workshop audience. Proceedings publication ----------------------- The proceedings of LPTI will be published in Electronic Proceedings in Theoretical Computer Science. The final proceedings will be published post-conference and will consist of revised versions of the accepted regular papers and invited talks. Preliminary proceedings will be made available at the conference in electronic form. _______________________________________________ Haskell mailing list Haskell@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell
