皆様、(重複して受け取られた場合は、御容赦ください。)
国際会議FLOPS2016 -- Functional and Logic Programming -- の
ポスターおよびデモ発表 の募集 & 参加募集
をお送りします。
FLOPS2016 は PPL2016 の直前に、比較的近い場所で開催されます。2件の招待講演:
Kazunori UEDA (Waseda University)
The exciting time and hard-won lessons of the Fifth Generation Computer Project
Atze Dijkstra (Utrecht University)
UHC: Coping with Compiler Complexity
のほか、興味深い話題でのチュートリアル3件も予定されています。
Andreas Abel, on Agda
Atze Dijkstra, on Attribute Grammars
Neng-Fa Zhou, on programming in Picat
FLOPS2016でポスターもしくはデモを行えば、招待講演者を含む参加者の方々
からのコメントを多く得られることと思います。
なお、これまで、日程は「2016/3/3-6 のうち 3日間程度」という曖昧な書き方を
していましたが、「2016/3/4-6」に確定させました。(PPL2016 は 3/7-9 です。)
多くの皆様のポスター/デモ発表、参加をお待ちしています。
--
亀山幸義 (筑波大学)
http://logic.cs.tsukuba.ac.jp/~kam
---------------------------------------------------------------------
Call for Participation and Posters/Demos
---------------
FLOPS 2016: 13th International Symposium on Functional and Logic Programming
March 4-6, 2016, Kochi, Japan http://www.info.kochi-tech.ac.jp/FLOPS2016/
Registration will be open on Monday, Dec 21, 2015.
Early registration deadline is Monday, Feb 8, 2016.
Poster/Demo abstract submission deadline is Monday, Jan 11, 2016.
FLOPS aims to bring together practitioners, researchers and
implementers of the declarative programming, to discuss mutually
interesting results and common problems: theoretical advances, their
implementations in language systems and tools, and applications of
these systems in practice. The scope includes all aspects of the
design, semantics, theory, applications, implementations, and teaching
of declarative programming. FLOPS specifically aims to
promote cross-fertilization between theory and practice and among
different styles of declarative programming.
In addition to the presentations of regular research papers, the FLOPS
program includes tutorials, as well as the poster/demo session for
demonstrating the tools and systems described during the talks and for
presenting works-in-progress and getting the feedback.
FLOPS has established a Best Paper award. The winner will be
announced at the symposium.
CALLS FOR POSTERS AND DEMONSTRATIONS
If you wish to present a poster at FLOPS, please send the plain text
abstract by e-mail to <flops2016(a)easychair.org> -- by January 11, 2016.
The abstract should include the title, the names of the authors and
their affiliation, along with enough details to judge its scope and
relevance. We will announce the accepted submissions on January 25,
2016. The format of the poster will be announced at that time.
Important Dates
* Submission due: January 11, 2016 (Monday), any time zone
* Notification: January 25, 2016 (Monday)
INVITED TALKS
Kazunori UEDA (Waseda University)
The exciting time and hard-won lessons of the Fifth Generation
Computer Project
Atze Dijkstra (Utrecht University)
UHC: Coping with Compiler Complexity
TUTORIALS
Andreas Abel, on Agda
Atze Dijkstra, on Attribute Grammars
Neng-Fa Zhou, on programming in Picat
ACCEPTED PAPERS
Ki Yung Ahn and Andrea Vezzosi.
Executable Relational Specifications of Polymorphic Type Systems using Prolog
Markus Triska.
The Boolean Constraint Solver of SWI-Prolog: System Description
Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers and Andrew Pond.
Proof Relevant Corecursive Resolution
Jay McCarthy, Burke Fetscher, Max New and Robert Bruce Findler.
A Coq Library For Internal Verification of Running-Times
Akimasa Morihata.
Incremental Computing with Abstract Data Structures
Wouter Swierstra and Joao Alpuim.
>From proposition to program: embedding the refinement calculus in Coq
Andre Van Delft and Anatoliy Kmetyuk.
Declarative Programming with Algebra
Ian Mackie and Shinya Sato.
An interaction net encoding of Godel's System T
Arthur Blot, Pierre-Evariste Dagand and Julia Lawall.
>From Sets to Bits in Coq
Jeremy Yallop, David Sheets and Anil Madhavapeddy.
Declarative foreign function binding through generic programming
Praveen Narayanan, Jacques Carette, Wren Romano,
Chung-Chieh Shan and Robert Zinkov.
Probabilistic inference by program transformation in Hakaru: System description
Francisco Javier Lopez-Fraguas, Manuel Montenegro and Juan Rodriguez-Hortala.
Polymorphic Types in Erlang Function Specifications
Remy Haemmerle, Pedro Lopez-Garcia, Umer Liqat, Maximiliano Klemen,
John Gallagher and Manuel V. Hermenegildo.
A Transformational Approach to Parametric Accumulated-cost Static Profiling
Taus Brock-Nannestad.
Space-efficient Planar Acyclicity Constraints: A Declarative Pearl
皆様、
来年6月に開催される国際会議FSCD 2016の(2nd) call for papers
です。
FSCD (Formal Structures for Computation and Deduction)は、
RTA (Rewriting Techniques and Applications)とTLCA (Typed Lambda
Calculi and Applications)を融合・発展させた新しい会議です。
論文の投稿をご検討いただけますと幸いです。
長谷川真人
京都大学数理解析研究所
--
SECOND CALL FOR PAPERS
First International Conference on Formal Structures for
Computation and Deduction (FSCD'16)
22 June -- 26 June 2016, Porto, Portugal
http://fscd2016.dcc.fc.up.pt/
[NEW: INVITED SPEAKERS, CONFERENCE AWARDS, SPECIAL ISSUE, SATELLITE EVENTS]
==========================================================================
IMPORTANT DATES
Abstract Submission: 29 January 2016
Paper Submission : 5 February 2016
Rebuttal : 21 - 23 March 2016
Notification : 6 April 2016
==========================================================================
FSCD (http://fscdconference.org/) covers all aspects of formal
structures for computation and deduction from theoretical foundations
to applications. Building on two communities, RTA (Rewriting
Techniques and Applications) and TLCA (Typed Lambda Calculi and
Applications), FSCD embraces their core topics and broadens their
scope to closely related areas in logics, proof theory and new
emerging models of computation such as quantum computing and homotopy
type theory. The name of the new conference comes from an unpublished
but important book by Gerard Huet that strongly influenced many
researchers in the area.
Suggested, but not exclusive, list of topics for submission are:
1 Calculi
* Lambda calculus
* Logics (first-order, higher-order, equational, modal, linear,
classical, constructive, etc.)
* Rewriting systems (string, term, higher-order, graph, conditional,
modulo, infinitary, etc.)
* Proof theory (natural deduction, sequent calculus, proof nets, etc.)
* Type theory and logical frameworks
* Homotopy type theory
2. Methods in Computation and Deduction
* Type systems (polymorphism, dependent, recursive, intersection,
session, etc.)
* Induction, coinduction
* Matching, unification, completion, orderings
* Strategies (normalization, completeness, etc.)
* Tree automata
* Model building and model checking
* Proof search (resolution, paramodulation, narrowing, focusing, etc.)
* Constraint solving and decision procedures
3. Semantics
* Operational semantics and abstract machines
* Game Semantics and applications
* Domain theory and categorical models
* Quantitative models (timing, probabilities, resources, etc.)
* Quantum computation and emerging models in computation
4. Algorithmic Analysis and Transformations of Formal Systems
* Type Inference and type checking
* Abstract Interpretation
* Complexity analysis and implicit computational complexity
* Checking termination, confluence, derivational complexity and
related properties
* Symbolic computation
5. Tools and Applications
* Programming and proof environments (proof assistants, automated
theorem prover, proof checkers, specialized provers, dependently
typed languages, etc.)
* Verification tools (abstract interpretation, termination,
confluence, specialized provers, etc.)
* Libraries for proof assistants and interactive theorem provers
(support for variable bindings, nominal, polynomial, equality, etc.)
* Case studies in proof assistants and interactive theorem provers
(formalizations, mechanizations, certifications)
* Certifications (theorems, rewriting techniques, etc.)
* Applications of formal systems inside and outside of CS (biology,
linguistics, physics, education, etc.)
INVITED SPEAKERS
Amal Ahmed (USA)
Ichiro Hasuo (Japan)
Gerard Huet (France)
Tobias Nipkow (Germany)
PROGRAM CHAIRS
Delia Kesner (Univ. Paris-Diderot)
Brigitte Pientka (McGill University)
fscd16(a)easychair.org
PROGRAM COMMITTEE
Andreas Abel (Gothenburg Univ.)
Zena Ariola (Univ. Oregon)
Patrick Baillot (CNRS & ENS Lyon)
Andrej Bauer (Univ. Ljubljana)
Eduardo Bonelli (Univ. Quilmes)
Patricia Bouyer (ENS Cachan)
Ugo Dal Lago (Univ. Bologna)
Nachum Dershowitz (Univ. Tel Aviv)
Mariangiola Dezani-Ciancaglini (Univ. Torino)
Derek Dreyer (MPI-SWS)
Santiago Figueira (Univ. Buenos Aires)
Marcelo Fiore (Univ. Cambridge)
Juergen Giesl (Univ. Aachen)
Nao Hirokawa (JAIST)
Martin Hofmann (LMU Munchen)
Delia Kesner (Univ. Paris-Diderot)
Naoki Kobayashi (Univ. Tokyo)
Dan Licata (Wesleyan Univ.)
Chris Lynch (Clarkson Univ.)
Narciso Marti-Oliet (Univ. Complutense)
Aart Middeldorp (Univ. Innsbruck)
Dale Miller (INRIA Saclay)
Cesar Munoz (NASA)
Vivek Nigam (Univ. Paraiba)
Brigitte Pientka (McGill Univ.)
Jakob Rehof (Univ. Dortmund)
Xavier Rival (ENS Paris)
Peter Selinger (Dalhousie Univ.)
Paula Severi (Univ. Leicester)
Jakob Grue Simonsen (Univ. Copenhagen)
Matthieu Sozeau (INRIA Rocquencourt)
Sophie Tison (Univ. Lille)
Femke van Raamsdonk (VU Univ. Amsterdam)
Nobuko Yoshida (Imperial College)
CONFERENCE CHAIR
Sandra Alves (University of Porto)
FSCD STEERING COMMITTEE:
Thorsten Altenkirch (Univ. Nottingham)
Gilles Dowek (INRIA)
Santiago Escobar (Univ. Politecnica de Valencia)
Maribel Fernandez (King's College London)
Masahito Hasegawa (Univ. Kyoto)
Hugo Herbelin (INRIA)
Nao Hirokawa (JAIST)
Luke Ong (Chair, Univ. Oxford)
Jens Palsberg (UCLA)
Kristoffer Rose (Two Sigma Investments)
Rene Thiemann (Univ. Innsbruck)
Pawel Urzyczyn (Univ. Warsaw)
Femke van Raamsdonk (VU Univ. Amsterdam)
PUBLICATION
The proceedings will be published as an electronic volume in the
Leibniz International Proceedings in Informatics (LIPIcs). All LIPIcs
proceedings are open access.
SUBMISSION GUIDELINES
Submissions can be made in two categories: regular research papers and
system descriptions.
Submissions of research papers must present original research which is
unpublished and not submitted elsewhere. They must not exceed 15 pages
(including figures and bibliography). Submissions of research papers
will be judged on originality, significance, correctness, and readability.
Submission of system descriptions must describe a working system which
has not been published or submitted elsewhere. They must not exceed 10
pages and should contain a link to a working system. System
descriptions will be judged on originality, significance, usefulness,
and readability.
Proofs of theoretical results that do not fit within the page limit,
executables of systems, code of case studies, benchmarks used to
evaluate a given system, should be made available, via a reference to
a website or in an appendix of the paper. Reviewers will be encouraged
to consider this additional material, but are not obliged
to. Submissions must be self-contained within the respective page
limit; considering the additional material should not be necessary to
assess the merits of a submission.
Submissions must be formatted using the LIPIcs style files using the
instructions at
http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/
A condition of submission is that, if accepted, one of the authors
must attend the conference to give the presentation.
Papers should be submitted via easychair. The submission site is at
https://easychair.org/conferences/?conf=fscd16
CONFERENCE AWARDS
Two awards will be selected: one for the best paper and another one for
the best student paper.
SPECIAL ISSUE
After the conference, authors of selected papers will be invited to submit
extended versions of their work to a special issue published in the
open-access
journal Logical Methods in Computer Science (LMCS).
SATELLITE EVENTS
The following meetings and workshops are colocated with FSCD 2016:
CL&C, DCM, HDRA, HOR, IFIP Working Group 1.6, ITRS, Linearity, LFMTP,
LSFA, UNIF, WPTE, WWV.
ORGANISING COMMITTEE
Sandra Alves (Univ. Porto)
Sabine Broda (Univ. Porto)
Jose Espirito-Santo (Univ. do Minho)
Mario Florido (Univ. Porto)
Nelma Moreira (Univ. Porto)
Luis Pinto (Univ. do Minho)
Rogerio Reis (Univ. Porto)
Ana Paula Tomas (Univ. Porto)
Pedro Vasconcelos (Univ. Porto)
皆様、
京大の末永です。12月8日(火)の 13:00 から
筑波大の海野さんに講演をお願いしています。
ご参加をお待ちしております。
末永幸平
--
日時:2015年12月8日(火) 13:00-14:00
場所:総合研究7号館情報3講義室
講演者:海野 広志(筑波大学大学院システム情報工学研究科コンピュータサイエンス専攻助教)
講演題目:帰納法によるホーン節制約解消法と関数型プログラムの関係的仕様自動検証への応用
概 要:Verification problems of programs in various paradigms (e.g.
imperative, functional, and concurrent) can be reduced to constraint
solving problems of Horn clauses over predicate variables, which
represent unknown inductive invariants to be inferred. In this talk,
we present a novel constraint solving method based on inductive
theorem proving: the method reduces Horn constraint solving to
validity checking of first-order formulas with inductively-defined
predicates,which are then checked by induction on the derivation of
the predicates. The method here uses an SMT solver to automate
inductive proofs.
The main advantage of our constraint solving method over existing
methods is that it can verify relational specifications (e.g., the
equivalence, associativity, commutativity, distributivity,
monotonicity, idempotency, and non-interference) where multiple
function calls need to be analyzed simultaneously. Furthermore, our
novel combination of Horn constraint solving and inductive theorem
proving extends the reach of
induction-based verification from pure total functions to impure
partial procedures in various paradigms. We have implemented a
prototype Horn constraint solver based on the proposed method and
obtained promising results in preliminary experiments.
--
Kohei Suenaga (末永幸平), Ph.D
Associate professor (准教授)
Graduate School of Informatics, Kyoto University
(京都大学情報学研究科)
ksuenaga(a)gmail.com
http://www.fos.kuis.kyoto-u.ac.jp/~ksuenaga/