Logic-ml

logic-ml@fos.kuis.kyoto-u.ac.jp

1792 discussions

Prof. Giovanni Sambin at NII Logic Seminar
by Makoto Tatsuta 16 Mar '15

16 Mar '15

Prof. Giovanni Sambin at NII Logic Seminar Date: March 23, 2015, 13:30--15:30 Place: National Institute of Informatics, Room 1716 (17th floor) 場所: 国立情報学研究所 17階 1716室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Speaker: Prof. Giovanni Sambin (University of Padova) Title: Realizability interpretation of topology Abstract: It is a fact of life that the classical notion of topological space can be obtained in a constructive (intuitionistic and predicative) way by starting from neighbourhoods and defining points as specific subsets of neighbourhoods. Beginning in the 80s, we introduced what is now called formal topology: a predicative and intuitionistic pointfree approach to topology. The key ingredient of a formal topology is a relation, called cover, between elements and subsets of a given set S of formal neighbourhoods, or observables. In the 90s, we showed that the cover relation of formal topologies can be generated by induction. Given a set of observables S, a family of sets I(a) set (a in S) and a family C(a,i) of subsets of S, for a in S and i in I(a), one can generate by induction the least cover such that every C(a,i) is a cover of a. We call this an axiom-set. Soon after, I also added a positivity relation, again between elements and subsets of S, which provides a way to introduce closed subsets in a pointfree way. We showed that positivity relations can be generated coinductively from an axiom-set. It turns out that generation, by induction and by coinduction, from axiom-sets is the only postulate over a very elementary foundation, which have been shown to admit a realizability interpretation. So to obtain a realizability interpretation of constructive topology one only need to find a realizability interpretation for the principle of generation from axiom-sets. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

TSSS (Tsukuba Software Science Seminar) at AIST Tsukuba, Mar. 23, 2015
by 山形賴之 11 Mar '15

11 Mar '15

Dear everyone, (apologies for multiple posts) I am pleased to announce another TSSS at AIST Tsukuba central, held Mar. 23, 2015. The program is as follows. Note that the largest canteen in AIST Tsukuba central is closed, so we have a long lunch break. You can eat and drink in the seminar room. The seminar is open to everyone, but please let me know by Mar. 19 if you want to attend. In particular, if you come by car, please let me know. 皆様、(重複投稿をお許し下さい) 2015年3月23日に産総研のつくばセンターでTSSSを開催いたします。プログラムは下記のとおりです。どなたでも参加できますが、参加予定の方はあらかじめ3月19日までに山形までご一報下さい。特にお車でお越しになる方は連絡をお願いします。なお、産総研の大食堂は現在閉鎖中です。外に食事に行けるよう昼休みを長めにとっています。セミナー室は飲食可能です。よろしくお願いします。 Tsukuba Software Science Seminar Date: Mar. 23, 2015 Place: National Institute of Advanced Industrial Science and Technology (AIST), Tsukuba central, AIST Tsukuba Headquarters and Information Technology Collaborative Research Center Map: http://www.aist.go.jp/aist_e/guidemap/tsukuba/tsukuba_map.html http://www.aist.go.jp/aist_e/guidemap/tsukuba/center/tsukuba_map_c.html 10:00 - 10:45 Runtime verification using a process algebra CSP, Yoriyuki Yamagata 10:45 - 11:00 Discussion 11:00 - 13:00 Break 13:00 - 13:45 Applying Formal Methods in Trust and Security systems, Liu Yang 13:45 - 14:00 Discussion 14:00 - 14:15 Break 14:15 - 15:00 Using Model Checking and Theorem Proving to Validate and Verify Cyber-Physical Systems, Chen-wei Wang 15:00 - 15:15 Discussion Title: Speaker: Yoriyuki Yamagata Abstract: A process algebra such as CSP, CCS, and pi-calculus is used to describe a concurrent system. In this talk, we introduce a tool called CSP_E, CSP for event monitoring. CSP_E tests a runtime log against a specification given by CSP, and report whether the log satisfies the given specification or not. CSP_E is implemented as a internal DSL within Scala programming language. Title: Using Model Checking and Theorem Proving to Validate and Verify Cyber-Physical Systems Speaker: Chen-wei Wang Abstract: In this talk I present part of the results that contribute to the research project "Certification of Safety-Critical Software-Intensive Systems" funded by the Ontario government. The project involves various application domains: biomedical, automotive, and nuclear. This talk focuses on the nuclear domain. Contributions are made by researchers at York University and McMaster University. I first present the use of an automated checking tools for Timed Transition Models (TTM) to model, simulate, and validate cyber-physical systems, with respect to discrete-time temporal properties. I then present the use of tabular expressions and the PVS theorem prover to model and verify function blocks that can be reused to build Programmable Logic Controllers (PLCs). In both approaches, I use function blocks supplied by the industrial standard 61131-3 for illustration. To conclude the talk, I report lessons that we learn and mention ongoing research. Title: Applying Formal Methods in Trust and Security systems Speaker: Liu Yang Abstract: Cyber-attack detection, defense and recovery are important topics in cybersecurity, but the ultimate goal of cybersecurity is to build attack-free systems. Security verification and building attack-free systems are very challenging tasks in view of the size and the complexity of the systems. In this talk, we will present our recent attempts in applying formal methods in modeling and verifying security protocols, security protocol implementations, malware in Android OS and even vulnerabilities. We will also discuss the challenges in applying formal methods in security and possible solutions. Lastly, we will introduce our recent research project “Securify: A Compositional Approach of Building Security Verified System”, which aims at building secure and verifiable systems ground-up. Short Bio: Dr Liu Yang graduated in 2005 with a Bachelor of Computing (Honours) in the National University of Singapore (NUS). In 2010, he obtained his PhD and started his post doctoral work in NUS, MIT and SUTD. In 2011, Dr Liu is awarded the Temasek Research Fellowship at NUS to be the Principal Investigator in the area of Cyber Security. In 2012 fall, he joined School of Computer Engineering, Nanyang Technological University as a Nanyang Assistant professor. Dr. Liu specializes in software verification, security and software engineering. His research has bridged the gap between the theory and practical usage of formal methods to evaluate the design and implementation of software for high assurance. His work led to the development of a state-of-the-art model checker, Process Analysis Toolkit (PAT). This tool is used by research institutions in over 70 countries for research and education. He has more than 100 publications and leading a research group of 30 people. -- 山形頼之独立行政法人産業技術総合研究所主任研究員 https://staff.aist.go.jp/yoriyuki.yamagata/

1 1

島根大学教授(任期なし) 公募【5/28締切】について
by Munehiro Iwami 11 Mar '15

11 Mar '15

皆様島根大学の岩見と申します。浜口先生の代理で「島根大学教授(任期なし) 公募【5/28締切】」の情報を送ります。 ------------------------------------------------------------------- 島根大学教授(任期なし) 公募【5/28締切】大学院総合理工学研究科情報システム学領域１．職名及び人数：教授　１名２．所属：島根大学大学院総合理工学研究科　情報システム学領域３．担当専門分野：情報科学／情報工学(ソフトウェア工学が望ましい) ４．担当予定授業科目　　　大学院総合理工学研究科情報システム学コースに関わる専門科目及び　　数理・情報システム学科（情報系）に関わる専門科目および全学基礎科目　　　大学院：専門分野に関連する科目，セミナー，特別研究　　　学　部：プログラミング関連および専門分野に関連する講義・演習科目，　　　　　　　　情報科学(全学基礎科目)，卒業研究５．任用予定年月日：平成２７年　１０月　１日以降のできるだけ早い時期６．応募資格　　　・博士の学位を有すること．　　・国籍は問わないが，日本語で授業ができること．７．提出書類　　　(1) 履歴書（写真貼付のこと）　　(2) 研究業績リスト　　　　研究費の獲得実績，および学会活動・社会活動の実績を含む　　(3) 論文別刷3編程度（コピー可）　　(4) 上記(3)の論文の概要（各論文について200字以内）　　(5) 教育研究に対する抱負　　(6) 業績を評価できる方2名の氏名及び連絡先　　応募書類は原則として返却しません。 ※ 提出書類に含まれる個人情報は，選考及び採用以外の目的には使用しま　せん。８．選考方法　　　書類選考及び必要に応じ本学において面接等を行います。その際の旅費・宿泊費は応募者の負担となります。また，島根大学では男女共同参画社会の実現を目指しています。「男女共同参画社会基本法」の趣旨に則り，業績（研究　業績，教育業績，社会的貢献等）及び人物の評価において同等と認められた場　合は女性を採用します。選考結果は応募者本人に通知します。９．応募締め切り：平成２７年５月２８日（木）必着　 10．応募書類の送付先　　〒690-8504　松江市西川津町１０６０　　島根大学大学院総合理工学研究科長　服部　泰直　　封筒の表に，「情報システム学領域教員応募書類在中」と朱書し，　　「（簡易）書留郵便」で郵送して下さい。 11．問い合わせ先　　島根大学大学院総合理工学研究科　情報システム学領域　領域長浜口　清治　　　TEL/FAX: 0852-32-6468 　　　E-mail: hama(a)cis.shimane-u.ac.jp (備　考) 本学は，「男女共同参画社会基本法」の趣旨に則り，男女共同参画を推進しています。以上． ------------------------------------------------------------------------ -- 以上、よろしくお願い致します。岩見宗弘島根大学総合理工学研究科情報システム学領域 E-mail: munehiro(a)cis.shimane-u.ac.jp

1 0

Workshop on Logic and Philosophy of Logic, March 19th(Thu)-20th(Fri), 2015
by Yuta Takahashi 10 Mar '15

10 Mar '15

--------------------------------------------------------------------- We apologize if you receive this message more than once. --------------------------------------------------------------------- The following Workshop on Logic and Philosophy of Logic is scheduled. 次のようなワークショップ「Workshop on Logic and Philosophy of Logic」を予定しております。参加自由です。 ---- Workshop on Logic and Philosophy of Logic 「論理学・論理哲学ワークショップ」 Date: March 19th(Thu)-20th(Fri), 2015 日時: 2015年3月19日(Thu)-20日(Fri) Place: Distance Learning Room (B4F), South Building, Mita campus of Keio University. 場所: 慶應大学三田キャンパス南館地下4階ディスタンスラーニングルーム (http://www.keio.ac.jp/en/maps/mita.html 13番の建物です。/ Building #13 on this map.) URL: http://ctj.keio.ac.jp/news/27 (*最新プログラムはこちらでご確認ください) ---- Tentative Program: 3/19: 13:00-13:10 Opening Remark, Mitsuhiro Okada (Keio University) 13:00-13:50 Makoto Fujiwara (Tohoku University, Department of Mathematics): "Constructive provability versus uniform provability in classical computable mathematics" 13:50-14:50 Giovanni Sambin (Dipartimento di Matematica Pura e Applicata, Università di Padova): "A single system for a plurality of logics" 14:50-15:20 Break 15:20-16:10 Gergei Bana (INRIA, France) "Fitting's model construction and computability" (joint work with Mitsuhiro Okada) 16:10-17:10 Sandra Laugier (Université Paris 1, Centre de Philosophie Contemporaine de la Sorbonne) "Rule-Following, Practice, and Forms of life" 17:10-17:30 Discussion 3/20: 10:30-11:10 Ukyo Suzuki (The University of Tokyo, Department of History and Philosophy of Science): "The Possibility of Predicative Arithmetic" (Talk in Japanese, possibly with English slides) 11:10-12:00 Shunsuke Yatabe (West Japan Railway Company): "Is truth a logical connective?" 12:00-13:30 Lunch Break 13:30-14:30 Mirja Hartimo (University of Jyväskylä, Department of Social Sciences and Philosophy) "Husserl and mathematics in the 1920s" 14:30-14:50 Break 14:50-15:50 Mathieu Marion (Université du Québec à Montréal, Philosophie Department) "Wittgenstein and Intuitionism: The Law of Excluded Middle and Following a Rule" 15:50-16:10 Break 16:10-17:00 Ryota Akiyoshi (Kyoto University, Department of Philosophy) "An interpretation of Brouwer’s argument of the bar induction via infinitary proof theory" 17:00-17:20 Concluding Discussion --------------------------------------------------------------------- Organisers: Ryota Akiyoshi (co-chair) Mitsuhiro Okada (co-chair) Yutaro Sugimoto Yuta Takahashi 主催: 慶應義塾大学「思考と行動判断」の研究拠点共催: 慶應義塾大学論理と感性のグローバル研究センター問合せ先: Mita Logic Seminar /「思考と行動判断」の研究拠点事務局 logic(a)abelard.flet.keio.ac.jp ------------------------- ABSTRACTS: Makoto Fujiwara "Constructive provability versus uniform provability in classical computable mathematics" So-called intuitionistic analysis EL is two-sorted intuitionistic arithmetic, which serves as system to formalize constructive mathematics. In this talk, we show that for any existence theorem T of some syntactical form, T is provable in EL if and only of T is uniformly provable in classical variant RCA of EL. From a philosophical point of view, it might be remarkable that all of our proofs are constructive, namely, they are just explicit syntactic translations. Thus we constructively (from a meta-perspective) establish the equivalence between constructive provability and classical uniform provability in RCA for a large number of existence theorems. ---- Giovanni Sambin "A single system for a plurality of logics" We propose a single, unified formulation for a wide variety of logics. This is achieved thorugh a sequent calculus UB for classical logic which uses a third structural sign, besides turnstile and comma, to denote active formulas in a context. Then, besides weakening and contraction, structural rules of UB include also some rules for the management of active formulas. All most common logics (classical, intuitionistic, paraconsistent, substructural, both in their intuitionistic and classical version) become literally (equivalent to) subsystems of UB. In other words, our previous approach showing that many logics could be seen as extensions of our basic logic B (JSL 2000), is now fully formal and internalized. Inference rules for all logical constants in UB are justified through the principle of reflection.This offers a single proof-theoretic semantics for all logical constants in all logics and confirms beyond doubts Dosen's principle saying that a logic is only determined by structural rules.A proof in one of the above logics is just a proof in UB which does not use some of the structural rules. We produce a cut-elimination procedure which respects structural rules and thus automatically becomes a cut-elimination procedure for all logics expressible as subsystems of UB.One benefit is that one can concentrate efforts on UB to improve both understanding and computational efficiency for a wide variety of logics. ---- Gergei Bana "Fitting’s model construction and computability" (joint work with Mitsuhiro Okada) We review Fitting’s embedding of classical logic into S4, that is, Fitting’s possible world semantics for classical logic.This is closely related to Cohen's forcing.Then we show how this construction naturally emerges when trying to formalize what a (malicious) agent can possibly computeor cannot compute from what is available to the agent as input.Finally, we illustrate how this construction helps us to carry out security proofs for cryptographic prot. ---- Sandra Laugier "Rule-Following, Practice, and Forms of life" TBA ---- Ukyo Suzuki "The Possibility of Predicative Arithmetic" (可述算術の可能性) In this talk, I will present an idea to find a non-revisionistic kind of interest in Edward Nelson’s Predicative Arithmetic. First, I’ll briefly summarize Predicative Arithmetic as a research program with Nelson’s own revisionistic motivation. Next, I’ll suggest Predicative Arithmetic can provide a formal model for Wittgenstein’s conception of mathematical proof as concept-formation. If my suggestion is correct, Predicative Arithmetic can give a Wittgensteinian answer to the so-called “paradox of inference” presented by Dummett. (この発表では、エドワード・ネルソン(1932-2014)の可述算術の興味を、非改訂主義的観点から捉えるアイデアを提示する。はじめに、可述算術という研究プログラムを、ネルソン自身の改訂主義的モチベーションと共に簡単に解説する。次に、可述算術が、ウィトゲンシュタインによって提示された、概念形成としての数学的証明という考え方に、形式的モデルを提供するものであることを示唆したい。この捉え方が正しければ、ダメットによって提示されたいわゆる「推論のパラドクス」に対して、可述算術は、ウィトゲンシュタイン的な解答を与える。) ---- Shunsuke Yatabe "Is truth a logical connective?" Truth theories like the Friedman-Sheard's truth theory ({\bf FS}) have two rules, T-in rule and T-out rule, about introduction and elimination of the truth predicate. They look like the introduction rule and the elimination rule of a logical connective. From the proof theoretic semantics viewpoint, one might think that the truth predicate is a logical connective which is governed by these two rules. >From this proof theoretic semantics viewpoint, the nature of truth is like deflationist's nature of truth. Additionally one of the most important things is that the truth predicate does not disturb the traceability of the argument from the premises to a conclusion. However, a crucial problem has been known: any criteria to be a logical connective, known as a ``harmony" of the introduction rule and the elimination rule, are not satisfied because of the $\omega$-inconsistency of FS. Such $\omega$-inconsistency is caused by the fact that the truth predicate enables us to define paradoxical formulae of seemingly infinite-length. These formulae can be regarded as coinductive objects in terms of computer science. The reason of the failure of the harmony is that these criteria are defined not for coinductively defined paradoxical formulae but for inductively defined formulae. In this talk, we examine how we can extend the criteria for harmony for coinductive formulae in terms of the inversion principle of proftheoretic semantics and corecursive functions in coinductive datatypes. --- Mirja Hartimo "Husserl and mathematics in the 1920s" The paper contextualizes Husserl’s writings on mathematics in the 1920s. It offers a look to Husserl’s library and in particular to the books on mathematics he owned and were published after 1917 but before 1929. Some of these books have reading marks showing that Husserl studied them. Four of them have been studied particularly carefully: Hilbert’s 1922 Neubegründung der Mathematik, Weyl’s article ”Die heutige Erkenntnislage in der Mathematik”(1925) and the book Philosophie der Mathematik und Naturwissenschaft (1926). The presentation will discuss the nature of Husserl’s reading marks on these items and then show how these influences can be seen in Husserl’s Formal and Transcendental Logic. --- Mathieu Marion "Wittgenstein and Intuitionism: The Law of Excluded Middle and Following a Rule" Wittgenstein attended a lecture by Brouwer in Vienna, in March 1928. Witness accounts by Herbert Feigl and Karl Menger and even Brouwer’s own testimony point to his interest, but there are few comments on typically intuitionistic topics, such as the critique of the unrestricted application of the Law of Excluded Middle, and the impact of intuitionism on his philosophy remains a controversial topic – nowadays, the opinion that it had none is quasi-universally accepted. In this paper, I shall begin by an overview of Wittgenstein’s relation to intuitionism, and then focus on two important topics, the Law of Excluded Middle and ‘following a rule’. On the first, I shall adduce evidence that he agreed with Brouwer’s reasoning, with his ‘weak counterexample’ using the decimal expansion of p (WVC, p. 71, AWL, p. 107 and M, p. 303). But Wittgenstein disagreed with Brouwer’s claim that the Law of Excluded Middle did not apply only for the ‘mathematics of the infinite’ (e. g ., PR § 73 or PG, p. 458); he believed that it does not apply even for elementary number theoretic equations. I shall argue that Wittgenstein’s position can only be understood in terms of the views laid out in the Tractatus Logico-Philosophicus, where a calculus of number-theoretic equations is presented: given that these are Scheinsätze and that logic applies to propositions, that calculus is meant to be logic-free. (This standpoint was further developed in the early 1930s, and led him, for example, to introduce a rule of uniqueness of a function defined by recursion, to do without mathematical induction.) On the second topic, Wittgenstein arrived at the following view of intuitionism in 1929: “each number has its individual properties […] Thus we never get away from the endlessly many individualities” (MS 106, p. 282). (This may not be an appropriate understanding of Brouwer’s views, but I shall leave this question aside.) But this raises a difficulty for the notion of a general rule and its application, since one “must recognize each time afresh that this rule may be applied […] No act of foresight can absolve me from this act of insight (Einsicht)” (PR, p. 171). See also Ambrose’s lectures notes, AWL, p. 133-134. We have here premises of the notorious ‘rule-following’ argument of PI §§ 143-242. (See, e.g., § 186 and LFM, p. 237 for a late critique of intuitionism along that line.) I shall end the paper by showing thus how the ‘rule-following’ argument embodies a critique of intuitionism, helping myself to recently published remarks by Waismann in his Oxford lectures on causality, and the current debate in analytic philosophy on ‘blind rule following’ sparks by paper by Paul Boghossian and Crispin Wright. --- Ryota Akiyoshi "An interpretation of Brouwer’s argument of the bar induction via infinitary proof theory" In a series of papers, Brouwer had developed intuitionistic analysis based on his concept of ``set”. In particular, he derived a key theorem called the fan theorem from another strong theorem called ``the bar induction”. Brouwer gave his argument to justify the bar induction in 1927, which is of great philosophical importance because it was one important source of the BHK-interpretation But the argument essentially depends on the assumption on the form of canonical proofs, so it has been considered as obscure or at least not evident. In this talk, we sketch an approach to understanding Brouwer’s argument via a tool in infinitary proof theory called the Omega-rule. This tool was introduced by Buchholz for ordinal analysis of impredicative theories. After explaining a historical background of the bar induction and basic notions in intuitionistic analysis, we introduce a version of the Omega-rule to analyze the bar induction and sketch how to embed the bar induction by it. By inspecting the embedding argument, we analyze the role of Brouwer’s assumption and conclude that his argument is mathematically well-motivated.

1 0

AIST Seminar on Software Reliability
by 山形賴之 10 Mar '15

10 Mar '15

皆様、産総研の山形です。重複して案内を受け取られた方にはお詫びいたします。下記の内容で、形式手法の実践的な側面に焦点を当てたセミナーを開催いたします。どなたでも参加できますが、参加される方は前日までに山形までご一報下さい。特にお車で参加される方はその旨お伝えください。 Dear everyone, I am pleased to announce "AIST Seminar on Software Reliability". This is a seminar on formal methods which is focused on industrial applications. The seminar is open to everyone, but please let me know by 3/19 if you want to join. In particular, if you come by a car, please let me know. AIST Seminar on Software Reliability date: Mar 20, 2015 Place: National Institute of Advanced Industrial Science and Technology (AIST), Tsukuba central, AIST Tsukuba Headquarters and Information Technology Collaborative Research Center Map: http://www.aist.go.jp/aist_e/guidemap/tsukuba/tsukuba_map.html http://www.aist.go.jp/aist_e/guidemap/tsukuba/center/tsukuba_map_c.html 14:00 - 14:45 Survey on concurrent model checkers, Yoriyuki Yamagata 14:45 - 15:00 Discussion 15:00 - 15:15 Break 15:15 - 16:00 Using Model Checking and Theorem Proving to Validate and Verify Cyber-Physical Systems, Chen-wei Wang 16:00 - 16:15 Discussion 16:15 - 16:30 Break 16:30 - 17:15 Applications of Model Checking on Different Systems using PAT, Liu Yang 17:15 - 17:30 Discussion 18:30 - Dinner Title: Survey on concurrent model checkers Speaker: Yoriyuki Yamagata Abstract: In this talk, we compare algorithms and performance benchmarks of concurrent model checkers Spin and LTSmin. The benchmarks suggests that LTSmin uses multicore quite efficiently, while Spin is optimized to singlecore. Title: Using Model Checking and Theorem Proving to Validate and Verify Cyber-Physical Systems Speaker: Chen-wei Wang Abstract: In this talk I present part of the results that contribute to the research project "Certification of Safety-Critical Software-Intensive Systems" funded by the Ontario government. The project involves various application domains: biomedical, automotive, and nuclear. This talk focuses on the nuclear domain. Contributions are made by researchers at York University and McMaster University. I first present the use of an automated checking tools for Timed Transition Models (TTM) to model, simulate, and validate cyber-physical systems, with respect to discrete-time temporal properties. I then present the use of tabular expressions and the PVS theorem prover to model and verify function blocks that can be reused to build Programmable Logic Controllers (PLCs). In both approaches, I use function blocks supplied by the industrial standard 61131-3 for illustration. To conclude the talk, I report lessons that we learn and mention ongoing research. Title: Applications of Model Checking on Different Systems using PAT Speaker: Liu Yang Abstract: Model checking is emerging as an effective software verification method with wide applications. However, still there are a lot research challenges in model checking techniques and in applying model checking techniques. To address these challenges, this talk presents our recent research contributions in the system modeling, efficient model checking algorithms development and the application of formal verification in concurrent objects design, cyber physical systems, security, multi-agent systems and pervasive systems. More important, we introduce a process analysis toolkit (PAT,www.patroot.com), which is a self-contained verification framework for specification, simulation and verification of concurrent, real-time and probabilistic systems. Since PAT is released 8 years ago, it has attracted 3500+ registered users world wide. Our vision is to achieve pervasive model checking so as to build a framework for realizing different verification techniques, and making model checking as planning, problem-solving, scheduling/services. Short Bio: Dr Liu Yang graduated in 2005 with a Bachelor of Computing (Honours) in the National University of Singapore (NUS). In 2010, he obtained his PhD and started his post doctoral work in NUS, MIT and SUTD. In 2011, Dr Liu is awarded the Temasek Research Fellowship at NUS to be the Principal Investigator in the area of Cyber Security. In 2012 fall, he joined School of Computer Engineering, Nanyang Technological University as a Nanyang Assistant professor. Dr. Liu specializes in software verification, security and software engineering. His research has bridged the gap between the theory and practical usage of formal methods to evaluate the design and implementation of software for high assurance. His work led to the development of a state-of-the-art model checker, Process Analysis Toolkit (PAT). This tool is used by research institutions in over 70 countries for research and education. He has more than 100 publications and leading a research group of 30 people. -- 山形頼之独立行政法人産業技術総合研究所主任研究員 https://staff.aist.go.jp/yoriyuki.yamagata/

2 1

Fwd: [TYPES/announce] CALCO 2015 : Last Call for Papers
by Ichiro Hasuo 09 Mar '15

09 Mar '15

========================================================= CALL FOR PAPERS: CALCO 2015 6th International Conference on Algebra and Coalgebra in Computer Science In cooperation with ACM SIGLOG June 24 - 26, 2015 Nijmegen, Netherlands http://coalg.org/calco15/ ========================================================== Abstract submission: March 22, 2015 Paper submission: April 2, 2015 Author notification: May 6, 2015 Final version due: June 3, 2015 ========================================================== -- SCOPE -- CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science. It is a high-level, bi-annual conference formed by joining the forces and reputations of CMCS (the International Workshop on Coalgebraic Methods in Computer Science), and WADT (the Workshop on Algebraic Development Techniques). Previous CALCO editions took place in Swansea (Wales, 2005), Bergen (Norway, 2007), Udine (Italy, 2009), Winchester (UK, 2011) and Warsaw (Poland, 2013). The sixth edition will be held in Nijmegen, the Netherlands, colocated with MFPS XXXI. -- INVITED SPEAKERS -- Andy Pitts - University of Cambridge, UK (joint with MFPS) Chris Heunen - University of Oxford, UK Matteo Mio - CNRS, ENS Lyon, FR Daniela Petrisan - Radboud University, Nijmegen, NL -- TOPICS OF INTEREST -- We invite submissions of technical papers that report results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. We encourage submissions in topics included or related to those listed below. * Abstract models and logics - Automata and languages - Categorical semantics - Modal logics - Relational systems - Graph transformation - Term rewriting * Specialised models and calculi - Hybrid, probabilistic, and timed systems - Calculi and models of concurrent, distributed, mobile, and context-aware computing - General systems theory and computational models (chemical, biological, etc.) * Algebraic and coalgebraic semantics - Abstract data types - Inductive and coinductive methods - Re-engineering techniques (program transformation) - Semantics of conceptual modelling methods and techniques - Semantics of programming languages * System specification and verification - Algebraic and coalgebraic specification - Formal testing and quality assurance - Validation and verification - Generative programming and model-driven development - Models, correctness and (re)configuration of hardware/middleware/architectures, - Process algebra * Corecursion in Programming Languages - Corecursion in logic / constraint / functional / answer set programming - Corecursive type inference - Coinductive methods for proving program properties - Implementing corecursion - Applications * Algebra and Coalgebra in quantum computing - Categorical semantics for quantum computing - Quantum calculi and programming languages - Foundational structures for quantum computing - Applications of quantum algebra -- NEW TOPIC -- This edition of CALCO will feature a new topic, and submission of papers in this area is particularly encouraged. * String Diagrams and Network Theory - Combinatorial approaches - Theory of PROPs and operads - Rewriting problems and higher-dimensional approaches - Automated reasoning with string diagrams - Applications of string diagrams - Connections with Control Theory, Engineering and Concurrency -- SUBMISSION GUIDELINES -- Prospective authors are invited to submit full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. Experience papers are welcome, but they must clearly present general lessons learned that would be of interest and benefit to a broad audience of both researchers and practitioners. Starting with CALCO 2015, proceedings will be published in the Dagstuhl LIPIcsâ EURO "Leibniz International Proceedings in Informatics series. Final papers should be no more than 15 pages long in the format specified by LIPIcs (http://www.dagstuhl.de/publikationen/lipics/anleitung-fuer-autoren/). It is recommended that submissions adhere to that format and length. Submissions that are clearly too long may be rejected immediately. Proofs omitted due to space limitations may be included in a clearly marked appendix. Both an abstract and the full paper must be submitted by their respective submission deadlines. A special issue of the open access journal Logical Methods in Computer Science (http://www.lmcs-online.org), containing extended versions of selected papers, is also being planned. Submissions will be handled via EasyChair https://www.easychair.org/conferences/?conf=calco2015 -- BEST PAPER AND BEST PRESENTATION AWARDS -- Following from the successful trial at CALCO 2013, this edition of CALCO will feature two awards: a best paper award whose recipients will be selected by the PC before the conference and a best presentation award, elected by the participants. -- IMPORTANT DATES -- Abstract submission: March 22, 2015 Paper submission: April 2, 2015 Author notification: May 6, 2015 Final version due: June 3, 2015 -- PROGRAMME COMMITTEE -- Samson Abramsky, University of Oxford, UK Andrej Bauer, University of Ljubljana, SLO Filippo Bonchi, CNRS and ENS Lyon, FR Corina Cirstea, University of Southampton, UK Andrea Corradini, University of Pisa, IT Ross Duncan, University of Strathclyde, UK MartÃ-n EscardÃ³, University of Birmingham, UK Dan Ghica, University of Birmingham, UK Helle Hansen, Radboud University Nijmegen and CWI, NL Ichiro Hasuo, University of Tokyo, JP Bart Jacobs, Radboud University Nijmegen, NL Bartek Klin, University of Warsaw, PL Barbara KÃ¶nig, University of Duisburg-Essen, D Dexter Kozen, Cornell, US Alexander Kurz, University of Leicester, UK Paul-AndrÃ(c) MelliÃ¨s, CNRS and University Paris VII, FR Stefan Milus, University of Erlangen-NÃ 1/4 rnberg, D Larry Moss (co-chair), Indiana University, US Dusko Pavlovic, University of Hawaii, US Daniela Petrisan, ENS Lyon, FR Damien Pous, ENS Lyon, FR John Power, University of Bath, UK Jan Rutten, Radboud University Nijmegen and CWI, NL Lutz Schroeder, University of Erlangen-Nuernberg, D Monika Seisenberger, University of Swansea, UK Alexandra Silva, Radboud University Nijmegen, NL Pawel Sobocinski (co-chair), University of Southampton, UK Ana Sokolova, University of Salzburg, AT Andrzej Tarlecki, University of Warsaw, PL -- ORGANISING COMMITTEE -- Alexandra Silva Bart Jacobs Nicole Messink Sam Staton -- PUBLICITY -- Fabio Zanasi -- LOCATION -- Nijmegen is the oldest city in the Netherlands and celebrated its 2,000th year of existence in 2005. It is situated in the eastern province of Gelderland, quite near to the German border. The latin name for Nijmegen, `NoviomagusÂ´, is a reminder of its Roman past. `NoviomagusÂ´ means `new marketÂ´ and refers to the right to hold a market as granted by the Romans. In the days of Charlemagne, the city was called `NumagaÂ´; later on, this became `NieumeghenÂ´ and `NimmegenÂ´. However, citizens born and bred in Nijmegen speak affectionately of `NimwegenÂ´. Nijmegen is one of the warmest cities of the Netherlands, especially during summer, when the highest temperatures in the country are usually measured in the triangle Roermond â EURO " Nijmegen â EURO " Eindhoven. The lack of north-south oriented mountain ranges in Europe make this area prone to sudden shifts in weather, giving the region a semi-continental climate. -- SATELLITE WORKSHOPS -- The workshop is intended to enable presentation of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute. CALCO 2015 will run together with the CALCO Early Ideas Workshop, with dedicated Early Ideas sessions at the end of each conference day. -- CALCO Early Ideas Overview -- The CALCO Early Ideas Workshop invites submissions on the same topics as the CALCO conference: reporting results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. The list of topics of particular interest is shown on the main CALCO 2015 page. CALCO Early Ideas presentations will be selected according to originality, significance, and general interest, on the basis of submitted 2-page short contributions. It can be work in progress, a summary of work submitted to a conference or workshop elsewhere, or work that in some other way might be interesting to the CALCO audience. A booklet with the accepted short contributions will be made available. We encourage PhD students and young researchers to submit Early Ideas papers to the CALCO 2015 Easychair site as for ordinary submissions, mentioning in the abstract that the paper is to be considered for an Early Ideas talk. =========== SIGLOG Anti-harassment Policy The open exchange of ideas and the freedom of thought and expression are central to the values and goals of SIGLOG. They require an environment that recognizes the inherent worth of every person and group. They flourish in communities that foster mutual understanding and embrace diversity. For these reasons, SIGLOG is committed to providing a harassment-free conference experience, and implements the ACM policy against harassment (see http://www.acm.org/sigs/volunteer_resources/officers_manual/anti-harassment…). Conference participants violating these standards may be sanctioned or expelled from the meeting, at the discretion of the conference organizers. Conference organizers are requested to report serious incidents to the SIGLOG Chair. =========

1 0

教員公募（名古屋大学情報科学研究科・助教）
by NISHIMURA Harumichi 08 Mar '15

08 Mar '15

logic-mlの皆様，名古屋大学の西村です．このたび情報科学研究科計算機数理科学専攻にて教員を公募することになりましたのでお知らせします．所属：名古屋大学大学院情報科学研究科計算機数理科学専攻情報数理モデル論講座募集人員：助教（テニュアトラック教員）1 名専門分野：数理情報学（量子計算理論，量子情報理論，量子測定理論，機械学習，数理統計学，統計的データ解析，組合せ最適化，アルゴリズム，およびその関連分野）着任時期：平成27 年10 月1 日以降のできるだけ早い時期応募締切：平成27年5月29日（金）必着詳細は添付のPDFをご覧ください．よろしくお願いいたします．名古屋大学大学院情報科学研究科西村治道

1 0

LCC 2015 - Call for Papers
by Nao Hirokawa 07 Mar '15

07 Mar '15

皆様第16回論理と計算量に関するワークショップ LCC 2015 の論文募集をご案内致します。今回は７月に京都で開催される ICALP / LICS のサテライトワークショップとして開催されます。ぜひ投稿をご検討下さい！廣川　直 (JAIST) ====================================================================== First Call for Papers LCC 2015 16th International Workshop on Logic and Computational Complexity July 4-5, 2015, Kyoto, Japan collocated with ICALP/LICS 2015 http://www.cs.swansea.ac.uk/lcc/ ====================================================================== LCC meetings are aimed at the foundational interconnections between logic and computational complexity, as present, for example, in implicit computational complexity (descriptive and type-theoretic methods); deductive formalisms as they relate to complexity (e.g. ramification, weak comprehension, bounded arithmetic, linear logic and resource logics); complexity aspects of finite model theory and databases; complexity-mindful program derivation and verification; computational complexity at higher type; and proof complexity. The program will consist of invited lectures as well as contributed talks selected by the Program Committee. IMPORTANT DATES: * submission April 19, 2015 * notification May 14, 2015 * workshop July 4-5, 2015 INVITED SPEAKERS: tba SUBMISSION: We welcome submissions of abstracts based on work submitted or published elsewhere, provided that all pertinent information is disclosed at submission time. There will be no formal reviewing as is usually understood in peer-reviewed conferences with published proceedings. The program committee checks relevance and may provide additional feedback. Submissions must be in English and in the form of an abstract of about 3-4 pages. All submissions should be submitted through Easychair at: https://easychair.org/conferences/?conf=lcc2015 PROGRAM COMMITTEE: * Albert Atserias (Universitat Politècnica de Catalunya, Barcelona) co-chair * Guillaume Bonfante (LORIA, Nancy) * Yijia Chen (Fudan University, Shanghai) * Ugo Dal Lago (Università degli Studi di Bologna) * Nao Hirokawa (JAIST, Nomi) co-chair * Antonina Kolokolova (Memorial University of Newfoundland) * Damiano Mazza (CNRS, LIPN - University Paris 13) * Georg Moser (University of Innsbruck) * Moritz Müller (Kurt Gödel Research Center for Mathematical Logic, Wien) * Benjamin Rossman (National Institute of Informatics, Tokyo) * Iddo Tzameret (Royal Holloway, University of London) * Heribert Vollmer (Leibniz Universität Hannover)

1 0

講演会 (Nadia Polikarpova氏)
by Atsushi Igarashi 06 Mar '15

06 Mar '15

皆様，京都大学の五十嵐です．以下の要領で MIT の Nadia Polikarpova さんの講演会を実施いたしますので，ふるってご参加ください．当日夕方には，簡単な懇親会も考えておりますので，興味のある方は五十嵐までご連絡ください．どうぞよろしくお願いいたします -- 五十嵐淳 (IGARASHI Atsushi) E-mail: igarashi(a)kuis.kyoto-u.ac.jp url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/ ---------------------------------------------------------------------- 日時: ３月１２日(木) 14:00〜15:00 場所: 京都大学吉田キャンパス総合研究７号館(旧工学部１０号館)１階１３１号室(セミナー室２) Title: A Fully Verified Container Library and Synthesis from Liquid Types Abstract: In this talk I will discuss two approaches to constructing provably correct programs: one is based on automated deductive verification, and the other one combines program synthesis and refinement types. The first part of my talk will present AutoProof: an automated deductive verifier for heap-manipulating object-oriented programs, as well as our experience using AutoProof to prove full functional correctness of a realistic general-purpose container library. While the comprehensive functionality and flexible design of container libraries pose nontrivial challenges to formal verification, our results indicate that verifying a realistic library (135 public methods, 8,400 LOC) is possible with moderate annotation overhead (1.4 lines of specification per LOC) and good performance (0.2 seconds per method on average). The second part of my talk builds upon the Liquid Types framework, which has been successfully used to verify a wide range of properties of functional programs with very little human interaction. The secret to this success is the encoding of program invariants using a combination of types and predicates from an SMT-decidable logic. I will discuss some ideas on how Liquid Type inference could be extended to infer program components, and ultimately synthesize programs that are correct by construction. Bio: Nadia Polikarpova is a postdoctoral researcher at MIT, where she works with Armando Solar-Lezama. She obtained her PhD at ETH Zurich in 2014. Her research interests are in program verification and synthesis.

1 0

Talk by G. Sambin and M. Maietti [13 Mar 15:30-]
by Shinya Katsumata 06 Mar '15

06 Mar '15

京都大学数理解析研究所の勝股です。 3月13日15:30から、University of PadovaのGiovanni Sambin氏とMaria Emilia Maietti氏に以下の講演をしていただくことになりましたので、ご連絡いたします。どうぞお気軽にお越しください。 ========== Time: 15:30-17:30, 13 Mar, 2015 Place: Rm 478, Research Building 2, Main Campus, Kyoto University http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (See 34) 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物) Speaker: Giovanni Sambin and Maria Emilia Maietti (University of Padova) Title: 1 A new foundation of constructive mathematics 50 years after Bishop's FCA 2 Why developing mathematics in a two-level foundation Abstract: --- 1. Giovanni Sambin --- A new foundation of constructive mathematics 50 years after Bishop's FCA Bishop's book Foundations of constructive analysis, 1967, briefly CFA, showed that constructive mathematics can be emancipated from the subjective views of its founder Brouwer. That single book started the process turning constructive mathematics into a rich and lively research field and community, as it is today. While standing on the shoulders of such giants, after almost fifty years it is our task to see further. Some epochal changes which took place after 1967 provide motivations and support. Outside mathematics: 1. Evolutionary thought has expanded its range of application and is now commonly accepted in science, except in mathematics. The main challenge awaiting us is to pass from a static, transcendent view of mathematics to a dynamic, human one. 2. The power of computers and other tools has enormously increased. Their active role in mathematical research will certainly also increase. This requires fully detailed formal systems for the foundation of mathematics. 3. Diffusion of information technology makes our world intensely connected. One feels the need of a framework which allows for a plurality of different world views. Moreover, inside mathematics: 1. new branches have been created, 2. other branches besides analysis have been constructivized, such as algebra and topology. The talk will give a preliminary view on a new foundational system inspired by these facts, first introduced in 2005 and later developed by M. E. Maietti and myself and called the Minimalist Foundation, shortly MF. Aims of MF include: 1. to permit the development of constructive mathematics, including topology, in agreement with a dynamic view (different levels of abstractions, real and ideal entities,...), 2. to provide a framework in which virtually all foundations of mathematics can be expressed by adding some assumptions (hence the adjective minimalist) and hence in particular a good setting for reverse mathematics, 3. to allow formalization of mathematics in a computer language, 4. to express the computational content of mathematics. More specifically MF keeps: 1. an effective notion of set different from an ideal notion of collection 2. the notions of operation (with instructions) distinct from that of function (without instructions), 3. a positive notion of existence We wish to know that MF is consistent by a proof, not by faith or feelings. One can prove much more than consistency for MF, namely a normalization theorem, a realizability interpretation, implementation in a proof-assistant. We conclude the talk by showing that one needs a theory with two levels of abstraction, thus providing a good introduction to Maietti's talk. --- 2. Maria Emilia Maietti --- Why developing mathematics in a two-level foundation We provide motivations for developing mathematics in a two-level formal system following the ideas put forward in joint work with G. Sambin in [MS05]. There we introduced the notion of two-level system to found constructive mathematics but it turned out that the same notion can be accomodated to develop mathematics in general with computer-aided formalization of its proofs. A main motivating example of such foundations is the Minimalist Foundation for constructive mathematics which was ideated in [MS05] and completed into two levels in [M09]. Its peculiarity is that it is compatible with most relevant constructive and classical foundations at the "right level". Another perculiarity is that its design makes use of different languages: mostly that of type theory, but also that of category theory and axiomatic set theory. [MS05] M.E. Maietti and G. Sambin "Toward a minimalist foundation for constructive mathematics" in L. Crosilla and P. Schuster eds., ''From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics", Oxford University Press, 2005 [M09] M.E. Maietti "A minimalist two-level foundation for constructive mathematics" Annals of Pure and Applied Logic 160(2009):319-354

1 0

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml