皆様
(English follows.)
早稲田大学の藤原誠です。
1. CTFM2016
先日ご案内させていた研究集会
Computability Theory and Foundations of Mathematics 2016
(2016年9月20日(火)~9月21日(水)、早稲田大学国際会議場)
の暫定プログラムが以下のページからご覧いただけます。
(プログラムに変更があった場合は随時更新いたします。)
http://www.sendailogic.com/CTFM2016/timetable.html
多くの方々にご参加いたたけることを期待しております。
本研究集会への参加は自由となっておりますので、どうぞふるってご参加下さい。
なお、20日夜の懇親会への参加を希望される方は9月12日までに以下より参加登録をお願いいたします。
http://www.sendailogic.com/CTFM2016/registration.html
詳しくは下記ホームページをご覧ください。
http://www.sendailogic.com/CTFM2016/
本研究集会に関するお問い合わせは以下へお願いいたします。
ctfm2016[at]fastmail.com
2. CTFM Companion Lecture
9月23日に東京工業大学にてStephan G. Simpson先生(Vanderbilt University)の講演が行われますのでこちらも合わせてご案内させていただきます。
詳しくは下記ホームページをご覧ください。
http://www.sendailogic.com/Titechworkshop/
どうぞよろしくお願いいたします。
==============================================================
Computability Theory and Foundations of Mathematics 2016
Waseda University, Tokyo, Japan, September 20 - 21, 2016
http://www.sendailogic.com/CTFM2016/
==============================================================
Computability Theory and Foundations of Mathematics (CTFM) aims to
develop computability theory and logical foundations of Mathematics. The
scope involves the topics Computability Theory, Reverse Mathematics,
Nonstandard Analysis, Proof Theory, Set Theory, Philosophy of
Mathematics, Constructive Mathematics, Theory of Randomness and
Computational Complexity Theory.
This is the sixth conference of the CTFM conference series:
http://www.jaist.ac.jp/CTFM/CTFM_SERIES/
This conference is supported by the Waseda Insitute for Advanced Study
and JSPS KAKENHI Grant Numbers JP26540001 and JP15H03634.
-------------------------------------------------------------------------------------------------------------------------
Invited speakers:
• David Belanger (National University of Singapore)
• Chi Tat Chong (National University of Singapore)
• Daisuke Ikegami (Tokyo Denki University)
• Wei Li (National University of Singapore)
• Kenshi Miyabe (Meiji University)
• Paul Shafer (Ghent University)
• Frank Stephan (National University of Singapore)
• Philip Welch (University of Bristol)
• Guohua Wu (Nanyang Technological University)
• Takeshi Yamazaki (Tohoku University)
• Yang Yue (National University of Singapore)
-------------------------------------------------------------------------------------------------------------------------
Registration deadline:
September 12, 2016.
(It will still be possible to register for the conference after the deadline, but in that case the participant cannot attend the banquet.
The banquet will be held on September 20 (18:30-20:30), at the same place as the conference venue.)
-------------------------------------------------------------------------------------------------------------------------
Organising Committee:
Makoto Fujiwara (Waseda University, co-chair)
Florian Pelupessy (Tohoku University)
Kazuyuki Tanaka (Tohoku University, co-chair)
Toshimichi Usuba (Waseda University)
Keita Yokoyama (JAIST)
------------------------------------------------------------------------------------------------------------------------
Participants are also invited to attend the Workshop on Mathematical Logic at the Tokyo Institute of Technology on September 23, which includes a CTFM companion lecture by Stephen G. Simpson:
http://www.sendailogic.com/Titechworkshop/
============================================
藤原 誠 (Makoto Fujiwara)
早稲田大学高等研究所
(Waseda Institute for Advanced Study, Waseda University)
E-mail: makoto_fujiwara(a)aoni.waseda.jp
============================================
皆様、(複数受け取られた場合はご容赦ください。)
東京大学の佐藤亮介です。
PEPM 2017 の締め切りが 9/30 まで延長されました。
新しい日程は次の通りです。
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
論文の締め切りまでまだ1ヶ月近くありますので、
是非、投稿をご検討ください。
--
東京大学大学院情報理工学系研究科
佐藤亮介
ryosuke(a)kb.is.s.u-tokyo.ac.jp
-------------------------------------------------------------------
FINAL CALL FOR PAPERS
Workshop on PARTIAL EVALUATION AND PROGRAM MANIPULATION (PEPM 2017)
NEWS: Deadline extension to 30th September (see below)
NEWS: Keynote talk by Neil Jones, DIKU (see below).
http://conf.researchr.org/home/PEPM-2017
Paris, France, January 16th - 17th, 2017
(co-located with POPL 2017)
PEPM is the premier forum for discussion of semantics-based program
manipulation. The first ACM SIGPLAN PEPM symposium took place in
1991, and meetings have been held in affiliation with POPL every year
since 2006.
PEPM 2017 will be based on a broad interpretation of semantics-based
program manipulation, reflecting the expanded scope of PEPM in recent
years beyond the traditionally covered areas of partial evaluation and
specialization. Specifically, PEPM 2017 will include practical
applications of program transformations such as refactoring tools, and
practical implementation techniques such as rule-based transformation
systems. In addition, the scope of PEPM covers manipulation and
transformations of program and system representations such as
structural and semantic models that occur in the context of
model-driven development. In order to maintain the dynamic and
interactive nature of PEPM and to encourage participation by
practitioners, we also solicit submissions of short papers, including
tool demonstrations, and of posters.
Scope
-----
Topics of interest for PEPM 2017 include, but are not limited to:
* Program and model manipulation techniques such as: supercompilation,
partial evaluation, fusion, on-the-fly program adaptation, active
libraries, program inversion, slicing, symbolic execution,
refactoring, decompilation, and obfuscation.
* Program analysis techniques that are used to drive program/model
manipulation such as: abstract interpretation, termination checking,
binding-time analysis, constraint solving, type systems, automated
testing and test case generation.
* Techniques that treat programs/models as data objects including
metaprogramming, generative programming, embedded domain-specific
languages, program synthesis by sketching and inductive programming,
staged computation, and model-driven program generation and
transformation.
* Application of the above techniques including case studies of
program manipulation in real-world (industrial, open-source)
projects and software development processes, descriptions of robust
tools capable of effectively handling realistic applications,
benchmarking. Examples of application domains include legacy
program understanding and transformation, DSL implementations,
visual languages and end-user programming, scientific computing,
middleware frameworks and infrastructure needed for distributed and
web-based applications, embedded and resource-limited computation,
and security.
This list of categories is not exhaustive, and we encourage
submissions describing applications of semantics-based program
manipulation techniques in new domains. If you have a question as to
whether a potential submission is within the scope of the workshop,
please contact the programme chairs.
Submission categories and guidelines
------------------------------------
Three kinds of submissions will be accepted: Regular Research Papers,
Short Papers and Posters.
* Regular Research Papers should describe new results, and will be
judged on originality, correctness, significance and clarity.
Regular research papers must not exceed 12 pages in ACM Proceedings
style (including appendix).
* Short Papers may include tool demonstrations and presentations of
exciting if not fully polished research, and of interesting
academic, industrial and open-source applications that are new or
unfamiliar. Short papers must not exceed 6 pages in ACM Proceedings
style (including appendix).
* Posters should describe work relevant to the PEPM community, and
must not exceed 2 pages in ACM Proceedings style. We invite poster
submissions that present early work not yet ready for submission to
a conference or journal, identify new research problems, showcase
tools and technologies developed by the author(s), or describe
student research projects.
At least one author of each accepted contribution must attend the
workshop and present the work. In the case of tool demonstration
papers, a live demonstration of the described tool is expected.
Suggested topics, evaluation criteria, and writing guidelines for both
research tool demonstration papers will be made available on the PEPM
2017 web site.
Student participants with accepted papers can apply for a SIGPLAN PAC
grant to help cover travel expenses and other support. PAC also
offers other support, such as for child-care expenses during the
meeting or for travel costs for companions of SIGPLAN members with
physical disabilities, as well as for travel from locations 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)
---------------------------------------------------------------------
Call for Papers
FTSCS 2016
5th International Workshop on Formal Techniques for Safety-Critical Systems
Tokyo, November 14/15, 2016
(satellite workshop of ICFEM 2016)
http://www.ftscs.org
---------------------------------------------------------------------
*** Deadline extension: Final submission deadline September 11 ***
*** Science of Computer Programming special issue ***
*** Springer CCIS proceedings ***
Aims and Scope:
There is an increasing demand for using formal methods to validate and
verify safety-critical systems in fields such as power generation and
distribution, avionics, automotive systems, and medical systems. In
particular, newer standards, such as DO-178C (avionics), ISO 26262
(automotive systems), IEC 62304 (medical devices), and CENELEC EN
50128 (railway systems), emphasize the need for formal methods and
model-based development, thereby speeding up the adaptation of such
methods in industry.
The aim of this workshop is to bring together researchers and engineers
who are interested in the application of formal and semi-formal methods
to improve the quality of safety-critical computer systems. FTSCS
strives to promote research and development of formal methods and
tools for industrial applications, and is particularly interested in
industrial applications of formal methods.
Specific topics include, but are not limited to:
* case studies and experience reports on the use of formal methods for
analyzing safety-critical systems, including avionics, automotive,
medical, railway, and other kinds of safety-critical and QoS-critical
systems
* methods, techniques and tools to support automated analysis,
certification, debugging, etc., of complex safety/QoS-critical systems
* analysis methods that address the limitations of formal methods in
industry (usability, scalability, etc.)
* formal analysis support for modeling languages used in industry,
such as AADL, Ptolemy, SysML, SCADE, Modelica, etc.
* code generation from validated models.
The workshop will provide a platform for discussions and the exchange of
innovative ideas, so submissions on work in progress are encouraged.
Submission:
We solicit submissions reporting on:
A- original research contributions (15 pages max, LNCS format);
B- applications and experiences (15 pages max, LNCS format);
C- surveys, comparisons, and state-of-the-art reports (15 pages max, LNCS);
D- tool papers (5 pages max, LNCS format);
E- position papers and work in progress (5 pages max, LNCS format)
related to the topics mentioned above.
All submissions must be original, unpublished, and not submitted
concurrently for publication elsewhere. Paper submission is done
via EasyChair at https://easychair.org/conferences/?conf=ftscs2016.
The final version of the paper must be prepared in LaTeX, adhering to
the LNCS format available at
http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0.
Publication:
All accepted papers will appear in the pre-proceedings of FTSCS 2016.
Accepted papers in the categories A-D above will appear in the
workshop proceedings that will be published as a volume in
Springer's CCIS series.
The authors of a selected subset of accepted papers will be invited to
submit extended versions of their papers to appear in a special issue
of the Science of Computer Programming journal.
Important dates:
Submission deadline: September 4, 2016; extended to September 11, 2016
Notification of acceptance: October 7, 2016
Workshop: November 14/15, 2016
Venue:
Tokyo, Japan
Program chairs:
Cyrille Artho AIST, Japan and KTH, Sweden
Peter Olveczky University of Oslo, Norway
Program committee:
Etienne Andre University Paris 13, France
Toshiaki Aoki JAIST, Japan
Cyrille Artho AIST, Japan and KTH, Sweden
Kyungmin Bae Pohang University of Science and Technology, Korea
Eun-Hye Choi AIST, Japan
Alessandro Fantechi University of Florence and ISTI-CNR, Pisa, Italy
Bernd Fischer Stellenbosch University, South Africa
Osman Hasan National University of Sciences & Technology, Pakistan
Klaus Havelund NASA JPL, USA
Jerome Hugues Institute for Space and Aeronautics Engineering, France
Marieke Huisman University of Twente, The Netherlands
Ralf Huuck Synopsys, Australia
Fuyuki Ishikawa National Institute of Informatics, Japan
Takashi Kitamura AIST, Japan
Alexander Knapp Augsburg University, Germany
Thierry Lecomte ClearSy System Engineering, France
Yang Liu Nanyang Technological University, Singapore
Robi Malik University of Waikato, New Zealand
Frederic Mallet INRIA Sophia Antipolis, France
Roberto Nardone University of Napoli "Federico II", Italy
Vivek Nigam Federal University of ParaÃba, Brazil
Thomas Noll RWTH Aachen University, Germany
Kazuhiro Ogata JAIST, Japan
Peter Olveczky University of Oslo, Norway
Charles Pecheur Universite catholique de Louvain, Belgium
Markus Roggenbach Swansea University, UK
Ralf Sasse ETH Zurich, Switzerland
Martina Seidl Johannes Kepler University, Austria
Oleg Sokolsky University of Pennsylvania, USA
Sofiene Tahar Concordia University, Canada
Carolyn Talcott SRI International, USA
Tatsuhiro Tsuchiya Osaka University, Japan
Andras Voros Budapest University of Technology and Economics,
Hungary
Chen-Wei Wang State University of New York (SUNY), Korea
Alan Wassyng McMaster University, Canada
Michael Whalen University of Minnesota, USA
Huibiao Zhu East China Normal University, China
--
Takashi KITAMURA
t.kitamura(a)aist.go.jp
http://staff.aist.go.jp/t.kitamura/
Tel: +81-72-751-9633, AIST internal: *33-272-79633
みなさま,
東京大学の蓮尾です.物理情報システム分野の一大イベント
CPS Week (来年はアメリカ開催です)のメイン会議の一つ,
HSCC の論文募集をお送りします.
コミュニティとしては,主にプログラム検証・システム検証の
人たちと,制御理論の人たちが,協力して研究を行っている
印象です.よろしければぜひ,論文投稿や参加をご検討ください.
どうかよろしくお願いいたします.
蓮尾 一郎
http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/
=======
20th International Conference on Hybrid Systems: Computation and Control
(HSCC)
April 18-21, 2017,
Pittsburgh, Pennsylvania, USA
URL: http://hscc2017.ece.illinois.edu/
Important dates
Paper Submission deadline: October 13, 2016 (firm, 11:59 pm UTC-12)
Notifications: December 20, 2016
Demo/poster submission: TBA
Camera-ready: February 17, 2017
Conference dates: April 18-21, 2017
Conference Scope
HSCC 2017 is the 20th in a series of conferences on all aspects of
hybrid systems. It is dedicated to advancing design and analysis
techniques that bridge control theory and computer science, and is
expanding to new domains in security and privacy and in systems
biology. The conference covers the range from theoretical results to
practical applications and experiences in cyber-physical systems
(CPS), mixed signal circuits, robotics, infrastructure networks, and
biological models. Topics of interest include, but are not limited to,
the following subjects:
* Mathematical foundations, computability and complexity
* Modeling paradigms and techniques
* Design, synthesis, planning, and control
* Analysis, verification, validation, and testing
* Programming and specification languages
* Network science and control over networks
* Security and privacy in cyberphysical systems
* Software tools
* Applications and case studies
HSCC 2017 will be part of the ninth Cyber Physical Systems Week (CPS
Week), and co- located with the International Conference on
Cyber-Physical Systems (ICCPS), Information Processing in Sensor
Networks (IPSN), the Real-Time and Embedded Technology and
Applications Symposium (RTAS), Conference on Internet-of-Things Design
and Implementation (IOTDI), and related workshops.
Regular papers: Submissions should present unpublished original
research, not under review elsewhere. Maximum 10 pages in 10pt,
two-column ACM format. This year we will enforce a light double-blind
reviewing process; the conference webpage will have more details.
Paper submissions should be preceded by an abstract (date TBA).
Authors of distinguished papers may be invited to submit an extended
version of their work for possible publication in a Special issue of a
leading journal. A Best Student Paper Award will be presented to the
author of the best paper written solely or primarily by a student.
Tool and case study papers: Tool Papers should describe an implemented
tool and its novelty. Maximum 6 pages in the 10pt, two-column ACM
format.
Demo/posters: Demo/poster descriptions are used for selecting
contributions for demo/poster session, and will not be published in
the proceedings. Maximum 2 pages, ACM format. Title should begin with
“Demo (Poster):”. Descriptions should be submitted to the
“Demonstrations and Posters” track at the submission website.
Submission website for papers:
https://easychair.org/conferences/?conf=hscc17
Repeatability evaluation: Authors of accepted papers will be invited
to participate in an optional repeatability evaluation process after
the camera-ready submission. Papers that pass will receive the
“artifact evaluated” badge and there will be a Best RE Award.
The official publication date may be up to two weeks before the conference.
Committees for HSCC 2017
Program Committee Chairs
Goran Frehse, Univ. Grenoble Alpes-Verimag
Sayan Mitra, Univ. of Illinois at Urbana-Champaign
Publicity Chair
Necmiye Ozay, Univ. of Michigan
Program Committee
Alessandro Abate, University of Oxford
Erika Abraham, RWTH Aachen
Matthias Althoff, TU München
Saurabh Amin, MIT
Murat Arcak, UC Berkeley
Shun-Ichi Azuma, Kyoto Univ.
Christel Baier, TU Dresden
Hamsa Balakrishnan, MIT
Ezio Bartocci, TU Wien
Calin Belta, Boston Univ.
Sergiy Bogomolov, IST Austria
Alessandro Cimatti, Fondazione Bruno Kessler
Alessandro D'Innocenzo, Univ. of L'Aquila
Thao Dang, VERIMAG, France
Anupam Datta, CMU
Jyotirmoy Deshmukh, Toyota
Arvind Easwaran, Nanyang Tech. Univ.
Georgios Fainekos, Arizona State Univ.
Lu Feng, Univ. of Virginia
Martin Fränzle, Carl von Ossietzky Univ. Oldenburg
Sicun Gao, MIT
Antoine Girard, Laboratoire des Signaux et Sys. CNRS
Ichiro Hasuo, Univ. of Tokyo
Franjo Ivancic, Google
Taylor T Johnson, Vanderbilt Univ.
James Kapinski, Toyota
Hadas Kress-Gazit, Cornell University
Marta Kwiatkowska, University of Oxford
Mircea Lazar, Eindhoven Univ. of Technology
Jun Liu, Univ. of Waterloo
Daniele Magazzeni, King's College London
Manuel Mazo Jr., TU Delft
Ian Mitchell, Univ. of British Columbia
Meeko Oishi, Univ. of New Mexico
Necmiye Ozay, Univ. of Michigan
André Platzer, CMU
Vinayak Prabhu, MPI-SWS
Maria Prandini, Politecnico di Milano
Akshay Rajhans, MathWorks
S Ramesh, General Motors
Grigore Rosu, Univ. of Illinois at Urbana-Champaign
Indranil Saha, IIT Kanpur
Ricardo Sanfelice, Univ. of Arizona
Scott Smolka, Stony Brook Univ.
Oleg Sokolsky, Univ. of Pennsylvania
Herbert Tanner, Univ. of Delaware
Ashish Tiwari, SRI
Ufuk Topcu, Univ. of Texas at Austin
Jana Tumova, Royal Institute of Technology
Ram Vasudevan, Univ. of Michigan
Steering Committee
Rajeev Alur, University of Pennsylvania
Werner Damm, OFFIS
John Lygeros, ETH Zurich
Oded Maler, Verimag
Paulo Tabuada, UCLA
Claire Tomlin, UC Berkeley
皆様
ルートヴィヒ・マクシミリアン大学ミュンヘンのJosef Berger先生、および
スワンジー大学のAnton Setzer先生・Bashar Igriedさんの講演のお知らせです。
どうぞふるってご参加ください。
問合せ先:
石原 哉
北陸先端科学技術大学院大学 情報科学系
e-mail: ishihara(a)jaist.ac.jp
-----------------------------------------------
* JAIST Logic Seminar Series *
* The lectures below are held as a part of JSPS Core-to-Core Program,
A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES
project CORCON.
(http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/)
Date: Tuesday 6 September, 2016, 13:30-17:00
Place: JAIST, Lecture room I2
(Access: http://www.jaist.ac.jp/english/location/access.html)
*LECTURE 1*
Speaker: Josef Berger (Ludwig-Maximilians-Universität München)
Title: The fan theorem and convexity (joint work with Gregor Svindland)
Abstract:
The fan theorem is the following statement:
(FAN) Let B be a decidable set of finite binary sequences.
Assume that every infinite binary sequence
has an initial part that belongs to B.
Then there exist an N such that every infinite binary
sequence has an initial part of length smaller than N
that belongs to B.
This axiom plays an important role in Intuitionism,
a philosophy of mathematics that was introduced by
the Dutch mathematician L.E.J. Brouwer. We work
in constructive mathematics in the tradition of Errett Bishop.
Here, the fan theorem is neither provable nor falsifiable.
Many theorems of analysis are equivalent
to the fan theorem. One example for such a theorem is:
(POS) Every positive-valued uniformly continuous function
on the unit interval has positive infimum.
In our paper 'Convexity and constructive infamy’ we have shown that,
under the additional condition of convexity of the function, POS is
constructively valid.
In this talk, we discuss to which extent this gives rise to
a notion of 'convex bars' and a corresponding constructively
valid 'convex fan theorem'.
*LECTURE 2*
Speaker: Anton Setzer and Bashar Igried (Swansea University)
Title: Coinductive Reasoning in Dependent Type Theory - Copatterns,
Objects, Processes
(part on Processes joint work with Bashar Igried)
Abstract:
When working in logic in computer science, one is very often confronted
with bisimulation. The reason for its importance is that in computer
science, one often reasons about interactive or concurrent programs.
Such programs can have infinite execution paths, and therefore
correspond to coinductive data types. The natural equality on coinductive
data types is bisimulation. Proofs of bisimulation form one of the main
principles for reasoning about coinductive data types.
However, bisimulation is often very difficult to understand and to teach.
This is in contrast to the principle of induction, where
there exists a well established tradition of carrying out proofs by
induction.
One goal of this talk is to demonstrate that one can reason about
coinductive data types in a similar way as one can reason inductively
about inductive
data types.
Reasoning about inductive data types can be done by pattern matching.
For instance
for reasoning about natural numbers one makes a case distinction on
whether the
argument is 0 or a successor. For coinductive data types the dual is
copattern
matching, which is essentially a case distinction on the observations
one can make for a coinductively defined set. For instance, streams have
observations head and tail, and one can introduce a stream by determining
its head and its tail.
We then look at examples of the use of coinductive data types. One is
the notion of an object, as it occurs in object-oriented program.
Objects are defined by their method calls, which are observations, so they
are defined coinductively. The final example will be the representation
of processes in dependent type theory, where we will refer
to the process algebra CSP.