Logic-ml December 2010

12 participants
15 discussions

東北大学ロジックセミナー
by YOKOYAMA Keita 13 Jan '11

13 Jan '11

皆様，東北大学の横山です．以下の日程でロジックセミナーを行いますので，ご興味のある方は是非ご参加ください．日時：10月29日(金) 場所：東北大学北青葉山キャンパス理学総合棟1201号室１４：４５〜１５：１５木原貴行（東北大学理学研究科）タイトル：Effectiveness for planar dendrites and dendroids １５：３０〜池上大祐（ヘルシンキ大学）タイトル：Infinite games with imperfect information セミナーの詳細につきましては， http://www.math.tohoku.ac.jp/~y-keita/friday-seminar/friday-seminar.html をご参照ください．横山啓太 -- Keita Yokoyama Mathematical Institute, Tohoku University Aoba, Sendai, JAPAN, 980-8578 y-keita(a)math.tohoku.ac.jp

1 4

Kobe Colloquium (talk by Sam Sanders)
by Makoto Kikuchi 29 Dec '10

29 Dec '10

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロクウィウムを開催します。日時：2011年1月20日（木）15:30 〜場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループプレゼンテーション室）講演者：Sam Sanders（東北大学）題目：A copy of several Reverse Mathematics アブストラクト： Reverse Mathematics (RM) is a program in the foundations of mathematics initiated by Friedman ([1, 2]) and developed extensively by Simpson ([4]). The aim of RM is to determine which minimal axioms prove theorems of ordinary mathematics. The main theme of RM is that a theorem of ordinary mathematics is either provable in RCA_0, or the theorem is equivalent to either WKL_0, ACA_0, ATR_0 or Π^1_1-CA_0. This equivalence is proved in RCA_0, the ‘base theory’ of RM. Moreover, each of these systems corresponds to a well-known foundational program in mathematics. Nonstandard Analysis has played an important role in RM ([3, 5]). We are interested in RM where equality is replaced by the relation ≈, i.e. equality up to infinitesimals. We obtain a ‘copy’ of the RM of WKL_0 and ACA_0 in a weak system of Nonstandard Analysis. Surprisingly, the same system is also a ‘copy’ of Constructive Reverse Mathematics. Our results have applications in Physics, Theoretical Computer Science, and the Philosophy of Science. References [1] Harvey Friedman, Some systems of second order arithmetic and their use, Proceedings of the International Congress of Mathematicians (Vancouver, B. C., 1974), vol. 1, Canad. Math. Congress, 1975, pp. 235–242. [2] Harvey Friedman, Systems of second order arithmetic with restricted induction I & II, Journal of Symbolic Logic, vol. 41 (1976), pp. 557–559. [3] H. Jerome Keisler, Nonstandard arithmetic and reverse mathematics, Bulletin of Symbolic Logic, vol. 12 (2006), no. 1, pp. 100–125. [4] Stephen G. Simpson, Subsystems of second order arithmetic, Perspectives in Mathematical Logic, Springer–Verlag, Berlin, 1999. [5] Kazuyuki Tanaka, The self-embedding theorem of WKL_0 and a non- standard method, Annals of Pure and Applied Logic, vol. 84 (1997), pp. 41–49. 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：菊池誠　mkikuchi(a)kobe-u.ac.jp

1 0

The 45th MLG Meeting: Program
by Takahiro Seki 26 Dec '10

26 Dec '10

第45回 MLG 数理論理学研究集会のご案内 (重複してお受け取りの際はご容赦ください。) 　新潟大学の関です。　2010年度MLG数理論理学研究集会（第45回）を下記の要領で開催します。　講演・宿泊の申し込みは締め切りましたが，参加することは可能です。なお，その場合，事前の申し込みは不要ですが，参加費（会場代）1,500円をいただきます。 =============================== 　第45回 MLG 研究集会開催要領 =============================== 　日時: 2011 年 1 月 6 日(木) 14:00 ～ 1 月 8 日(土) 12:20 　場所: KKR湯沢ゆきぐに（ＪＲ上越新幹線越後湯沢駅西口より徒歩約8分）　　　　〒949-6101 新潟県南魚沼郡湯沢町湯沢2574 　　　　URL : http://www.kkryuzawa.com/ 　MLG45ホームページ：　http://math.ed.niigata-u.ac.jp/~seki/MLG45/ 　講演プログラム： 1月6日（木） 14:00～14:10　開会・事務連絡 14:10～14:50　関　隆宏（新潟大学）　On Halldén-completeness of relevant modal logics 14:50～15:30　角谷良彦（東京大学）　Curry-Howard correspondence with modalities based on Kripke semantics 15:50～16:30　岩波　克（東京工業大学）　直観主義二階命題論理の性質について 16:30～17:10　金子　守（筑波大学）　A measure of inference in classical and intuitionistic logics (with N.-Y. Suzuki) 1月7日（金） 9:00～ 9:40　竹村　亮（慶應義塾大学）　オイラー図推論の証明論的分析：自然演繹への翻訳と正規形証明 9:40～10:20　照井一成（京都大学）　　未　定 10:30～11:10　倉橋太志（神戸大学）　一階述語証明可能性論理における２つの意味論について 11:10～11:50　佐々木克巳（南山大学）　様相論理Grzにおける標準形の論理式とexactモデル 13:00～13:40　丸山善宏（京都大学）　Duality, monad, and topological category: Concrete-categorical investigation into algebraic-logical structures 13:40～14:20　横山啓太（東北大学）　Reverse mathematics in several frameworks 14:30～15:10　髙野道夫（新潟大学）　真理値が集合である２値論理 15:20～16:00　古森雄一（千葉大学）　変数を区別しないときの述語論理の正規化定理 16:00～16:40　小野寛晰（北陸先端科学技術大学院大学）　　未　定 1月8日（土） 9:20～10:00　松尾亮太（名古屋大学）　繰り返しゲームにおける複雑な戦略 10:00～10:40　鈴木信行（静岡大学）　ゲーム理論に由来する直観主義的多様相述語論理およびそのKripke型意味論 10:50～11:30　鹿島　亮（東京工業大学）　Canonical models for some modal logics 11:30～12:10　志村立矢（日本大学）　Some cut-free multi-modal logics 12:10～12:20　事務連絡・閉会 --- 関　隆宏新潟大学企画戦略本部評価センター Tel : 025-262-6088 Fax : 025-262-6248 E-mail : tseki(a)adm.niigata-u.ac.jp

1 0

[TACL 2011] First call for papers
by tacl2011＠lif.univ-mrs.fr 24 Dec '10

24 Dec '10

Dear colleague, please, find below the TACL 2011 first call for papers. We strongly hope to meet you in Marseilles during next July. Best regards, Luigi Santocanale, Yves Lafont, Nicola Olivetti, TACL 2011 local organisers =============================================================================== TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2011) =============================================================================== 26-30 July 2011 Universités Aix-Marseille I-II-III, France http://www.lif.univ-mrs.fr/tacl2011/ The Fifth International Conference on Topology, Algebra and Categories in Logic is dedicated to the memory of Leo Esakia (1934-2010). Scope ----- Studying logics via semantics is a well-established and very active branch of mathematical logic, with many applications, in computer science and elsewhere. The area is characterized by results, tools and techniques stemming from various fields, including universal algebra, topology, category theory, order, and model theory. The program of the conference TACL 2011 will focus on three interconnecting mathematical themes central to the semantical study of logics and their applications: algebraic, categorical, and topological methods. This is the fifth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL). Earlier installments of this conference have been organized in Tbilisi (2003), Barcelona (2005), Oxford (2007), Amsterdam (2009). Featured topics --------------- Contributed talks can deal with any topic dealing with the use of algebraic, categorical or topological methods in either logic or computer science. This includes, but is not limited to, the following areas: * Algebraic structures in CS * Algebraic logic * Coalgebra * Categorical methods in logic * Domain theory * Fuzzy and many-valued logics * Lattice theory * Lattices with operators * Modal logics * Non-classical logics * Ordered topological spaces * Ordered algebraic structures * Pointfree topology * Proofs and Types * Residuated structures * Semantics * Stone-type dualities * Substructural logics * Topological semantics of modal logic Submissions ----------- Contributed presentations will be of two types: o 20 minutes long presentations in parallel sessions and o featured, 30 minutes long, plenary presentations. The submission of an abstract will be required to be selected for a contributed presentation of either kind. While preference will be given to new work, results that have already been published or presented elsewhere will also be considered. More information on the submission procedure will be made available soon. Important dates --------------- April 18, 2011: Abstract submission deadline May 20, 2011: Notification to authors July 26-30, 2011: Conference Program Committee ----------------- Guram Bezhanishvili, New Mexico State University Petr Cintula, Academy of Sciences of the Czech Republic Thierry Coquand, University of Gothenburg Mai Gehrke, Radboud University, Nijmegen Silvio Ghilardi, Università degli Studi di Milano Rob Goldblatt, Victoria University, Wellington Martin Hyland, King's College, Cambridge Ramon Jansana, Universitat de Barcelona Achim Jung (PC co-chair), University of Birmingham Alexander Kurz, University of Leicester Yves Lafont, Université Aix-Marseille II Tadeusz Litak, University of Leicester Paul-André Melliès, CNRS Paris Diderot George Metcalfe, Universität Bern Nicola Olivetti, Université Aix-Marseille III Hiroakira Ono, Japan Advanced Institute of Science and Technology Luigi Santocanale, Université Aix-Marseille I Kazushige Terui, Kyoto University Costantine Tsinakis, Vanderbilt University Yde Venema (PC co-chair), University of Amsterdam Friedrich Wehrung, Université de Caen Michael Zakharyaschev, University of London More Information ---------------- If you have any queries please send them to the conference email address: tacl2011(a)lif.univ-mrs.fr ===============================================================================

1 0

[TACL 2011] First call for papers
by Hiroakira Ono 21 Dec '10

21 Dec '10

= = = = = = = ======================================================================== TOPOLOGY, ALGEBRA AND CATEGORIES IN LOGIC (TACL 2011) = = = = = = = ======================================================================== 26-30 July 2011 Universités Aix-Marseille I-II-III, France http://www.lif.univ-mrs.fr/tacl2011/ Scope ----- Studying logics via semantics is a well-established and very active branch of mathematical logic, with many applications, in computer science and elsewhere. The area is characterized by results, tools and techniques stemming from various fields, including universal algebra, topology, category theory, order, and model theory. The program of the conference TACL 2011 will focus on three interconnecting mathematical themes central to the semantical study of logics and their applications: algebraic, categorical, and topological methods. This is the fifth conference in the series Topology, Algebra and Categories in Logic (TACL, formerly TANCL). Earlier installments of this conference have been organized in Tbilisi (2003), Barcelona (2005), Oxford (2007), Amsterdam (2009). Featured topics --------------- Contributed talks can deal with any topic dealing with the use of algebraic, categorical or topological methods in either logic or computer science. This includes, but is not limited to, the following areas: * Algebraic structures in CS * Algebraic logic * Coalgebra * Categorical methods in logic * Domain theory * Fuzzy and many-valued logics * Lattice theory * Lattices with operators * Modal logics * Non-classical logics * Ordered topological spaces * Ordered algebraic structures * Pointfree topology * Proofs and Types * Residuated structures * Semantics * Stone-type dualities * Substructural logics * Topological semantics of modal logic Submissions ----------- Contributed presentations will be of two types: 20 minutes long presentations in parallel sessions and featured, 30 minutes long, plenary presentations. The submission of an abstract of 1-4 pages is required to be selected for a contributed presentation of either kind. While preference will be given to new work, results that have already been published or presented elsewhere will also be considered. More information on the submission procedure is available on the conference website. Important dates --------------- April 18, 2011: Abstract submission deadline May 20, 2011: Notification to authors July 26-30, 2011: Conference Program Committee ----------------- Guram Bezhanishvili, New Mexico State University Petr Cintula, Academy of Sciences of the Czech Republic Thierry Coquand, University of Gothenburg Mai Gehrke, Radboud University, Nijmegen Silvio Ghilardi, Università degli Studi di Milano Rob Goldblatt, Victoria University, Wellington Martin Hyland, King's College, Cambridge Ramon Jansana, Universitat de Barcelona Achim Jung (PC co-chair), University of Birmingham Alexander Kurz, University of Leicester Yves Lafont, Université Aix-Marseille II Tadeusz Litak, University of Leicester Paul-André Melliès, CNRS Paris Diderot George Metcalfe, Universität Bern Nicola Olivetti, Université Aix-Marseille III Hiroakira Ono, Japan Advanced Institute of Science and Technology Luigi Santocanale, Université Aix-Marseille I Kazushige Terui, Kyoto University Costantine Tsinakis, Vanderbilt University Yde Venema (PC co-chair), University of Amsterdam Friedrich Wehrung, Université de Caen Michael Zakharyaschev, University of London More Information ---------------- If you have any queries please send them to the conference email address: tacl2011(a)lif.univ-mrs.fr Luigi Santocanale, Yves Lafont, Nicola Olivetti, TACL 2011 local organisers ============================================================

1 0

New book
by Torben Brauner 21 Dec '10

21 Dec '10

BOOK ANNOUNCEMENT Hybrid Logic and its Proof-Theory by Torben Braüner Applied Logic Series, Vol. 37 Springer, 2011 ISBN 978-94-007-0001-7 * This is the first book-length treatment of hybrid logic and its proof-theory. Hybrid logic is an extension of ordinary modal logic which allows explicit reference to individual points in a model (where the points represent times, possible worlds, states in a computer, or something else). This is useful for many applications, for example when reasoning about time one often wants to formulate a series of statements about what happens at specific times. * There is little consensus about proof-theory for ordinary modal logic. Many modal-logical proof systems lack important properties and the relationships between proof systems for different modal logics are often unclear. In the present book we demonstrate that hybrid-logical proof-theory remedies these deficiencies by giving a spectrum of well-behaved proof systems (natural deduction, Gentzen, tableau, and axiom systems) for a spectrum of different hybrid logics (propositional, first-order, intensional first-order, and intuitionistic). * All these proof systems can be motivated independently, but the fact that the systems can be given in a uniform way shows that hybrid logic and hybrid-logical proof-theory is a natural enterprise. * Further information can be found at http://www.springer.com/philosophy/logic+and+philosophy+of+language/book/97…

1 0

Adventures of Categories: Applied Category Theory Colloquium
by Ichiro Hasuo 13 Dec '10

13 Dec '10

*** 重複ご容赦下さい．また，興味のありそうな方にぜひご転送ください *** みなさま，こんにちは！京都大学数理解析研究所の蓮尾と申します． Adventures of Categories: Applied Category Theory Colloquium というプロジェクトの一環として，10月から12月にかけて6回，京大数理研で講演会を行っています．今週の金曜日の講演は中岡宏行氏鹿児島大学理学部数理情報科学科による， An Introduction to Triangulated Categories です．ホモロジー代数で用いられる三角圏の概念が立ち現れる様子を，予備知識を仮定せずお話いただきます．講演会の詳細については以下を，またプロジェクトの詳細については http://www.kurims.kyoto-u.ac.jp/~ichiro/AdvCat/Home.html をご覧ください．みなさまのお越しを歓迎します．それでは！ "Adventures of Categories" 参加者有志： Piet Hut，Craig Pastro，荒井迅，一宮尚志，西郷甲矢人，中岡宏行，長谷川真人，浜野正浩，春名太一，平岡裕章，蓮尾一郎 /////////////////////////////////////////////////////////////////////////////////////////// Date, Time: 14:00-15:00, Friday 17 Dec, 2010 Place: Room 111, RIMS, Kyoto University http://www.kurims.kyoto-u.ac.jp/en/access-01.html 京都大学数理解析研究所 1階 111号室 http://www.kurims.kyoto-u.ac.jp/ja/access-01.html Speaker: Hiroyuki Nakaoka (Kagoshima University) Title: An Introduction to Triangulated Categories Abstract: Homological Algebra is seemingly the most standard area of category theory used in Mathematics. Though classically the platform for homological algebra was an abelian category, recent advanced results involve its 'cousin', a triangulated category. In this talk, we will see briefly how the notions of an abelian and a triangulated category appears, and open the gate to the homological algebra. //////////////////////////////////////////////////////////////////////// =============== "Adventures of Categories" プロジェクトについて http://www.kurims.kyoto-u.ac.jp/~ichiro/AdvCat/Home.html 数学における異分野協働の実験場として，数学の中でもそのわかりにくさにおいて定評のある圏論 category theory をコアに据えて， - 純粋数学における圏論ユーザー - 応用数学における圏論ユーザー - 興味はあるがこれまで足を踏み入れる機会のなかった圏論の to-be ユーザー (この立場から，プリンストン高等研究所の学際研究担当，Piet Hut 教授にも参加いただきます) の3者の交流の機会とすべく今回のプロジェクトを企画しました． 6回の講演会の中から， - いろいろな数学の分野でどのように圏論が使われているのか？ - 各分野間の知識移転によって，どのような成果が得られるか？ - 圏論的手法が有効な他の応用分野は？ - テクニカルに素人の方に対して，圏論をどのように説明し，アピールすることができるか？というような問に対して，何らかの答えが浮かび上がるのを期待しています．興味のおありの方，ご来聴を歓迎いたします！ Adventures of Categories というタイトルは，本プロジェクト参加者の西郷甲矢人さんの発案です．A.N. Whitehead の本， Adventures of Ideas にかかっています．次回以降，代数学・幾何学における圏論や数理物理学における圏論，さらに Hut 教授による講演 "How to motivate non-mathematicians to explore category theory"など，企画しております．こちらもどうかご期待ください．日程は 10/1, 10/22, 11/5, 11/19, 12/3, 12/17 です． # 本プロジェクトは，(独) 科学技術振興機構さきがけプログラムから支援 # を受けています． http://math.jst.go.jp/

1 0

Second International Conference on Order, Algebra and Logics (2nd announcement)
by Order Algebra Logic 10 Dec '10

10 Dec '10

==================================================================== SECOND ANNOUNCEMENT ==================================================================== SECOND INTERNATIONAL CONFERENCE ON ORDER ALGEBRA AND LOGICS (Honoring Ralph McKenzie, Hiroakira Ono and Andrzej Wronski on the occasion of their 70th Birthdays) http://2oal.tcs.uj.edu.pl June 6-10, 2011, Krakow, POLAND ==================================================================== This meeting shares the goals of the conference with the same title, held Nashville in June 2007, and continues the tradition of related conferences in Prague, Novi Sad and Szeged. Recent years have witnessed increased research activity on the interface between logic and universal algebra. In particular, the use of algebraic methods has proved to be fruitful in the study of non-classical logics as well as in investigations related to the constraint satisfaction problem. The purpose of the conference is to bring together researchers from these fields to foster collaboration and further research. FEATURED AREAS The featured areas include, but are not limited to, the following (in alphabetical order): - Algebraic logic - Algorithmic problems in algebra - Applications of universal algebra to logics - Applications of universal algebra to the constraint satisfaction problem - Complexity and other algorithmic problems - Duality theory for algebraic structures - Lattice theory - Modal logics - Non-classical logics - Ordered algebraic structures - Ordered sets - Proof theory - Residuated structures and substructural logics - Tame congruence theory and applications - Topological methods in algebra and logic The scientific program consists of 50-minute plenary lectures, and 20-minute contributed talks. INVITED SPEAKERS - Libor Barto (Prague/Hamilton) - Nikolaos Galatos (Denver) - Mai Gehrke (Nijmegen) - Keith Kearnes (Boulder) - Tomasz Kowalski (Lisbon) - Tadeusz Litak (Leicester) - Petar Markovic (Novi Sad) - Miklos Maroti (Szeged) - Vicenzo Marra (Milan) - George McNulty (Columbia) - George Metcalfe (Bern) - Daniele Mundici (Florence) - Kazushige Terui (Kyoto) - Matthew Valeriote (Hamilton) - Ross Willard (Waterloo) ORGANIZERS - Wieslaw Dziobiak, University of Puerto Rico, Mayaguez - Pawel Idziak, Jagiellonian University - Marcin Kozik, Jagiellonian University - Constantine Tsinakis, Vanderbilt University PAPER SUBMISSION Researchers wishing to present a 20-30 minute contributed talk at the conference are invited to submit a short version of their paper via the EasyChair conference management system. (Please refer to the conference web site for detailed instructions.) These short papers must be submitted as .pdf files, have a length of two to three pages, and clearly describe the topic and contribution of the proposed talk. The first page should include title, names of authors, the affiliation, address, and email of the corresponding author. The submission procedure will also require the authors to provide some keywords describing the topic of the paper; and a plain text abstract (200 words maximum). Hence, keywords and abstract should not be included in the paper proper. The paper and the abstract must be submitted by 23:59 CET February 14th, 2011. The authors of accepted papers will be notified by March 28th, 2011. REGISTRATION FEE The conference fee will be 500 PLN prior to April 29th, 2011, and 750 PLN thereafter. The fee will cover costs related to conference activities, including coffee breaks and the banquet, but it will not cover the hotel and meal expenses of the conference participants. The banquet fee for each accompanying person is 150 PLN. Fees can be paid in advance by money transfer, or by cash at the conference site. NO CREDIT CARDS WILL BE ACCEPTED. (Further details regarding registration and payment procedures will be provided at the beginning of 2011.) LODGING Lodging information will be posted in the conference website early at the beginning of January 2011 IMPORTANT DATES - Submission of paper and abstract: February 14, 2011 - Acceptance notification: March 28, 2011 - Deadline to register with a registration fee of 500 PLN: April 29, 2011 (The registration fee after this date is 750 PLN - Conference: June 6-10, 2011 FURTHER INFORMATION Information about the conference can be found at the conference web site at "http://2oal.tcs.uj.edu.pl/index.html" (without the quotes). E-mail inquiries should be directed "2oal(a)tcs.uj.edu.pl".

1 0

Kobe Colloquium (talk by Dmitri Shakhmatov)
by Joerg Brendle 09 Dec '10

09 Dec '10

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロクウィウムを開催します。日時：2010年12月16日（木）15:10 〜場所：神戸大学自然科学総合研究棟3号館4階421室（渕野グループプレゼンテーション室）講演者：Dmitri Shakhmatov（愛媛大学）題目：A Kronecker-Weyl theorem for subsets of abelian groups アブストラクト： Let N be the set of non-negative integer numbers, T the circle group and c the cardinality of the continuum. Given an abelian group G of size at most 2^c and a countable family F of infinite subsets of G, we construct ``Baire many'' monomorphisms pi: G to T ^c such that pi(E) is dense in { y in T^c : ny=0 } whenever n in N , E in F, nE = {0} and { x in E : mx=g } is finite for all g in G and m such that n = mk for some k in N \ {1} . We apply this result to obtain an algebraic description of countable potentially dense subsets of abelian groups, thereby making a significant progress towards a solution of a problem of Markov going back to 1944. A particular case of our result yields a positive answer to a problem of Tkachenko and Yaschenko (2002). Applications to group actions and discrete flows on T^cont, diophantine approximation, Bohr topologies and Bohr compactifications are also provided. 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：ブレンドレヨーグ brendle(a)kurt.scitec.kobe-u.ac.jp

1 0

Prof. Olivier Danvy Lecture at NII Logic Seminar
by Makoto Tatsuta 09 Dec '10

09 Dec '10

Prof. Olivier Danvy Lecture at NII Logic Seminar Date: December 16, 2010, 14:00--16:00 Place: National Institute of Informatics, Room 2005 (20th floor) 場所: 国立情報学研究所 20階 2005室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/introduce/access1-j.shtml) Speaker: Prof. Olivier Danvy (University of Aarhus) Title: Small-step and Big-step Aspects of Computation (A Walk in the Semantic Park) Abstract: On the one hand, there are the De Morgan laws: it is clear how to repeatedly apply them to put a proposition in, say, negational normal form, with many small computational steps. On the other hand, such a normal form can be obtained with one big computational step by recursive descent. On the second hand, there is the lambda-calculus: it is clear how to repeatedly apply its contraction rules to put a lambda-term in, say, weak-head normal form, if one exists, with many small computational steps. On the other hand, such a normal form can be obtained with one big computational step by recursive descent. On the third hand, there are also abstract machines: state transition systems that will obligingly yields normal forms as well, if they exist. There is no fourth hand in this talk: our goal is not to monkey with computation, but to demonstrate a profound structural unity in the various styles of semantic artifacts that have been proposed to specify computation: as a calculus with a reduction strategy, as a small-step system of proof rules, as a small-step system of reductions in contexts, as a small-step abstract machine, as a big-step abstract machine, as a continuation-passing big-step evaluation function, and as a direct-style big-step evaluation function. In the course of this talk, we will materialize this unity by using off-the-shelf program transformations to constructively inter-derive semantic artifacts for deterministic sequential programming languages, or, to be precise, their representation as functional programs. 問合せ先: 龍田真 (国立情報学研究所) e-mail: tatsuta(a)nii.ac.jp http://research.nii.ac.jp/~tatsuta

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml December 2010