皆様,
# 重複して受け取られた場合はご容赦ください.
京都大学の末永と申します.
スウェーデンのハルムスタード大学の Walid Taha さんが
ポスドクを募集しています.Taha さんは最近 Acumen という
ハイブリッドシステムのモデリング言語を作っておられるのですが,
その言語のコンパイラについて研究するポストのようです.
興味をお持ちの方は Taha さんに直接コンタクトをお取りください.
末永幸平
--
Postdoc position on compiling hybrid differential equations
An NSF CPS project on Robot Design is building foundations and tools
for the simulation of hybrid (continuous/discrete) systems. The
project has an opening a postdoctoral research with Professor Taha at
Rice University.…
[View More] The successful candidate will design and evaluate
compilation strategies forenclosure-based solvers for hybrid
differential equations, and will be part of the team developing the
Acumen modeling language.
Applicants for this position should have strong skills and interest in
functional programming theory and practice; property-based testing;
performance analysis; and Scala. Excellent communication and
collaboration skills are required for both independent and
collaborative team work. Priority will be given to applicants who
already hold a doctoral degree in Computer Science, but applicants
with suitable skills and interests who hold a doctorate in
Mathematics, Physics, Electrical Engineering or Mechanical Engineering
are also encouraged to apply. Desirable experience includes
experience with writing numerical codes, interval and enclosure
methods, domain theory, operational semantics, formal verification,
differential equations, hybrid/impulsive differential equations, and
mechanical hardware design and control, especially in the context of
robotics. Desirable skills also include facility with Haskell, OCaml,
ML, Scheme, Mathematica, Maple, OpenGL, Matlab, Simulink, and other
modeling and simulation tools.
The position is for one year, renewable to two years, and is subject
to the availability of funding. The successful applicant will likely
spend part of their time in Halmstad, Sweden (50%) as part of the
collaboration. Successful applicants may start by the end of December
2013 or early March 2014.
The deadline for applications is November 29th, 2013. Application for
this position should be sent directly to Professor Taha by email. The
title of the email should be (without quotes) "Postdoc Position on
Compiling Hybrid Differential Equations". The application should
consist of one, self-contained PDF attachment. The application should
include 1) a brief cover letter including motivation for the
application, 2) a CV, and 3) a list of names of references. It is also
suggested that the application include online pointers to previous
publications or software produced by the applicant.
--
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/
[View Less]
皆様、
北陸先端科学技術大学院大学の佐野勝彦です。
CMCS'14 のCall for Papersをお送りいたします。
今回のCMCS'14では東京大学の蓮尾一郎さんの招待講演があります。
皆様、どうぞふるって論文をご投稿ください。締切は2014年1月です。
----------------------------------
Call for Papers
12th International Workshop on
Coalgebraic Methods in Computer Science (CMCS'14)
5 - 6 April 2014, Grenoble, France
http://www.coalg.org/cmcs14
Objectives and scope
-------------------
Established in 1998, the CMCS workshops aim …
[View More]to bring together researchers
with a common interest in the theory of coalgebras, their logics, and their
applications. As the workshop series strives to maintain breadth in its scope,
areas of interest include neighbouring fields as well. Topics of interest
include, but are not limited to, the following:
- The theory of coalgebras (including set theoretic and categorical
approaches)
- Coalgebras as computational and semantical models (for
programming languages, dynamical systems, term rewriting, etc.)
- Coalgebras in (functional, object-oriented, concurrent, and constraint)
programming
- Model checking, theorem proving and deductive verification
using coalgebraic techniques
- Coalgebraic data types, type systems and
behavioural typing
- Proof principles and (coinductive) definitions for
coalgebras (e.g. with bisimulations or invariants)
- Coalgebras and algebras
- Coalgebraic specification and verification
- Coalgebras and (modal) logic
- Coalgebra and control theory (notably of discrete event
and hybrid systems)
- Coalgebra in quantum computing
- Coalgebra and game theory
- Tools exploiting colgebraic techniques
Venue and event
---------------
CMCS??14 will be held in Grenoble, France, co-located with ETAPS 2014 on
5 - 6 April 2014.
Important dates
---------------
Abstract regular papers 6 January 2014
Submission regular papers 10 January 2014 (strict)
Notification regular papers 14 February 2014
Camera-ready copy 21 February 2014
Submission short contributions 23 February 2014 (strict)
Notification short contributions 9 March 2014
Invited speakers
----------------
Ichiro Hasuo, University of Tokyo, JP
Marina Lenisa, University of Udine, IT
Programme committee
-------------------
Andreas Abel, Ludwig-Maximilians-University Munich, DE
Davide Ancona, University of Genova, IT
Adriana Balan, University Politehnica of Bucharest, RO
Marta Bilkova, Charles University, CZ
Filippo Bonchi, LIP ENS-Lyon, FR
Marcello Bonsangue (chair), Leiden University, NL
Joerg Endrullis, Free University of Amsterdam, NL
Remy Haemmerle, University Politecnica de Madrid, SP
Bart Jacobs, Radboud University Nijmegen, NL???
Dexter Kozen, Cornell University, US
Bartek Klin, University of Warsaw, PL
Pierre Lescanne, ENS Lyon, FR
Stefan Milius, University of Erlangen-Nurenberg, DE
Rob Myers, Technical University of Braunschweig, DE
Dirk Pattinson, Australian National University, AU
Daniela Petrisan, University of Leicester, UK
Grigore Rosu, University of Illinois at Urbana-Champaign, US
Katsuhiko Sano, JAIST, Nomi, JP
Monika Seisenberger, Swansea University, UK
Ana Sokolova, University of Salzburg, AT
Publicity chair
---------------
Alexandra Silva, Radboud University Nijmegen, NL
PC chair
--------
Marcello Bonsangue, Leiden University, NL
Steering committee
------------------
Jiri Adamek, Technical University of Braunschweig, DE
Marcello Bonsangue, Leiden University, NL
Corina Cirstea, University of Southampton, UK
H. Peter Gumm (chair), University of Marburg, DE
Bart Jacobs, Radboud University Nijmegen, NL
Alexander Kurz, University of Leicester, UK
Marina Lenisa, University of Udine, IT
Ugo Montanari, University of Pisa, IT
Larry Moss, Indiana University, US
Dirk Pattinson, Australian National University, AU
John Power, University of Bath, UK
Horst Reichel, Technical University of Dresden, DE
Jan Rutten, CWI and Radboud University Nijmegen, NL
Lutz Schroeder, University of Erlangen-Nurenberg, DE
Submission guidelines
---------------------
We solicit two types of contributions: regular papers and short contributions.
Regular papers must be original, unpublished, and not submitted for
publication elsewhere. They should not exceed 20 pages in length in Springer
LNCS style. Short contributions may describe work in progress, or summarise
work submitted to a conference or workshop elsewhere. They should be no more
than two pages. Regular papers and short contributions should be submitted
electronically as a PDF file via the Easychair system at
http://www.easychair.org/conferences/?conf=cmcs2014.
The proceedings of CMCS 2014 will include all accepted regular papers and
will be published post-conference as a Springer volume in the IFIP-LNCS
series. Accepted short contributions will be bundled in a technical report.
[View Less]
皆様
リュブリャナ大学のAndrej Bauer教授の講演のお知らせです。
ふるってご参加ください。
問合せ先:
石原 哉
北陸先端科学技術大学院大学 情報科学研究科
e-mail: ishihara(a)jaist.ac.jp
--------------------------------------------------
* JAIST Logic Seminar Series *
* This seminar is held as a part of the EU FP7 Marie Curie Actions
IRSES project COMPUTAL (http://computal.uni-trier.de/).
Date: Friday 20 September, 2013, 15:00-17:00
Place: JAIST, Collaboration room 6 (I-57g)
(Access: http://www.jaist.ac.jp/english/location/access.html)
Speaker: Professor …
[View More]Andrej Bauer (University of Ljubljana, Slovenia)
Title: A higher inductive construction of the real numbers
Abstract:
Homotopy type theory [1] is a foundation of mathematics based on
Martin-Löf type
theory extended with the Univalence axiom and higher inductive types. The
latter allow us to present mathematical objects as inductive types generated
by point and path constructors. For instance, the circle is represented by a
type with a point and a loop satisfying the "circle induction" principle.
In the first part I shall review higher inductive types.
In the second part of the talk I shall look at a higher inductive
construction
of real numbers. Ordinary higher inductive types do not seem to suffice --
instead we have to use a higher inductive-inductive definition which
simultaneously constructs the reals and a proximity relation on them. We
thus
obtain a type of real numbers which satisfies a principle of "real
induction".
We can prove properties of reals by induction!
From a logical point of view the construction is interesting because
it avoids the
axiom of choice, impredicativity (powersets), and excluded middle.
Nevertheless, the resulting theory still allows us to develop the basics of
real analysis as usual.
The work described in the talk is joint work of the members of the Univalent
foundations project [2].
References:
[1] Univalent Foundations Project: "Homotopy type theory: Univalent
foundations of Mathematics",
http://homotopytypetheory.org/book/
[2] Univalent Foundations Project, Institute for Advanced Study, Princeton,
http://www.math.ias.edu/sp/univalent
--
Professor Hajime Ishihara
School of Information Science
Japan Advanced Institute of Science and Technology
1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan
Tel: +81-761-51-1206
Fax: +81-761-51-1149
ishihara(a)jaist.ac.jp
http://www.jaist.ac.jp/~ishihara
[View Less]
Kobe Colloquium on Logic, Statistics and Informatics
以下の要領でコロキウムを開催します。
日時:2013年10月25日(金)15:10-16:10
講演者:Bernhard Koenig
場所:神戸大学自然科学総合研究棟3号館4階421室(プレゼンテーション室)
============================================================
題目:
Variations of Laver's indestructibility result and some applications
アブストラクト:
We show that a supercompact cardinal kappa can be made indestructible under
a
class of forcings which is slightly larger than Laver's class of
kappa-directed closed forcings. We go on to …
[View More]discuss how this slight
strengthening over Laver's original result can be used for some
interesting new consistency results.
============================================================
交通:阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」
行きに乗車,「神大本部工学部前」停留所下車,徒歩すぐ.
http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm
[View Less]
第 34 回 NUEセミナーのお知らせ
東北大学・電気通信研究所・外山研究室ではNUEセミナーを開催しています。
テーマはプログラム理論や定理自動証明を中心に、情報科学の理論的なさまざ
まな話題をとりあげています。興味をおもちの方はどなたでもフラリと気楽に
おたちより下さい。
*********************************************
日時: 10月29日(火) 13:30 -- 14:30
場所: 東北大学・電気通信研究所・2号館・2階 セミナー室 (W214)
*********************************************
講演
話題提供者: Vincent van Oostrom (Utrecht University)
題目: Z Syntax-Free Developments
概要: We introduce the Z-property for abstract rewriting systems, and
show that it …
[View More]can be used to prove confluence of several well-known
term rewrite systems (terminating or not, and overlapping or not), in
particular:
- the applicative TRS for associativity: (xy)z -> x(yz);
- the applicative TRS for self-distributivity: (xy)z -> xz(yz);
- lambda-calculus with beta-reduction: (\x.M)N -> M[x:=N].
Turning to meta-theoretical properties, we first show that the
Z-propery allows to recover the traditionally syntactically defined
notion of (super)development/multistep in a syntax-free way. To that
end, we show the equivalence between the Z-property and Takahashi's
angle-property. Next, we showing that the Z-property not only
entails confluence, but also the existence of a hyper-cofinal
strategy.
We conclude by presenting further (non-)examples of rewrite systems
having the Z-property, and some open questions.
(joint work with Patrick Dehornoy)
==============================================
NUEセミナーに関する問い合わせは以下にどうぞ。
外山 芳人
〒980-8577 仙台市 青葉区 片平 2-1-1
東北大学 電気通信研究所
TEL 022 217 5449
FAX 022 217 5452
MAIL toyama(a)nue.riec.tohoku.ac.jp
[View Less]
sonoteno, logic-ml, jssst-ppl
各メーリングリストの皆様、
京都産業大学理学部数理科学科の三好博之です。
先ほど、蓮尾さんから東京大学でのBakhadyr Khoussainovさんの
講演会のアナウンスが有りましたが、京都産業大学でも
明日10/23(水) 14:00-15:00 に京都産業大学万有館
(バスプールからエスカレーターを2つ乗り継いだ正面の建物)
3階セミナー室にて談話会が行われます。東大の講演より
少し時間が短いですがAbstractを見るとだいたい同じ内容のようです。
アナウンスが遅れて申し訳ありませんが皆様の参加をお待ちしています。
三好博之
*******************************************
Speaker
Bakhadyr Khoussainov 氏(University of Auckland)
Title
An excursion to computable structures
Date
2013年10月23日(水) 14:00--15:00
Place
万有館3階セミナー室
…
[View More]Abstract
In this talk we introduce the concept of computable structure.
We discuss the history of the subject, present motivation, topics
and questions that have developed the subject over many years.
We explain the role of computability and logic in the study of various
mathematical structures. The talk will be quite informal, non-technical,
and will contain a good amount of examples and explanations.
*******************************************
三好博之
2013/10/22 Ichiro Hasuo <ichiro(a)is.s.u-tokyo.ac.jp>:
> Dear all,
>
> Friday next week we have Bakhadyr Khoussainov from
> University of Auckland visiting us in U Tokyo and making a talk
> on automatic structures (NB. automaton -> automatic).
> No registration needed. See you there!
>
> Best regards,
> Ichiro Hasuo
> http://www-mmm.is.s.u-tokyo.ac.jp/?plain=false&lang=en&pos=seminar
>
> ______________________________
>
> Fri 1 November 2013, 10:30-12:00
>
> Bakhadyr Khoussainov (U. Auckland),
> An excursion from computable to automatic structures
>
> 理学部7号館地下 007教室 (いつもの1階の部屋ではありません)
> Room 007 (underground floor), School of Science Bldg. No. 7
>
> アクセス: https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html
> Access: http://www-mmm.is.s.u-tokyo.ac.jp/
>
> In this talk we introduce two classes of structures: computable structures and
> automatic structures. We present several examples, theorems, research topics
> in the areas, and discuss their motivations, proofs and importance.
> The goal will
> be to make a transition from computable to automatic structures with an eye
> towards decidability. We also give some historical perspective.
>
> --
> このメールは Google グループのグループ「sonoteno」の登録者に送られています。
> このグループから退会し、メールの受信を停止するには、sonoteno+unsubscribe(a)googlegroups.com にメールを送信します。
> このグループに投稿するには、sonoteno(a)googlegroups.com にメールを送信してください。
> http://groups.google.com/group/sonoteno からこのグループにアクセスしてください。
[View Less]
Dear all,
Friday next week we have Bakhadyr Khoussainov from
University of Auckland visiting us in U Tokyo and making a talk
on automatic structures (NB. automaton -> automatic).
No registration needed. See you there!
Best regards,
Ichiro Hasuo
http://www-mmm.is.s.u-tokyo.ac.jp/?plain=false&lang=en&pos=seminar
______________________________
Fri 1 November 2013, 10:30-12:00
Bakhadyr Khoussainov (U. Auckland),
An excursion from computable to automatic structures
理学部7号館地下 007教室 (いつ…
[View More]もの1階の部屋ではありません)
Room 007 (underground floor), School of Science Bldg. No. 7
アクセス: https://www-mmm.is.s.u-tokyo.ac.jp/indexj.html
Access: http://www-mmm.is.s.u-tokyo.ac.jp/
In this talk we introduce two classes of structures: computable structures and
automatic structures. We present several examples, theorems, research topics
in the areas, and discuss their motivations, proofs and importance.
The goal will
be to make a transition from computable to automatic structures with an eye
towards decidability. We also give some historical perspective.
[View Less]