Logic-ml May 2018

10 participants
13 discussions

Tutorial by William Byrd at Kyoto Univ.
by Atsushi Igarashi 09 May '18

09 May '18

皆様，京都大学の五十嵐です．現在FLOPS2018で来日中の William E. Byrd さんに，来週の水・木の二日間にわたって，京大で relational programming のチュートリアルをして頂くことになりました． Dr. Racket をインストールしたノートＰＣを持ってくると，より楽しめるとのことです :-) 二日間にわたっていますが，二日目も最初に復習から入るようにお願いしました．一部だけでもどうぞ．ふるってご参加ください． ========================================================================== 日時: 5/16(水) 10:30〜15:30 (途中昼休みあり) 5/17(木) 10:30〜15:30 (途中昼休みあり) 会場: 京都大学吉田キャンパス総合研究７号館会議室(１階１２３号室) William E. Byrd Department of Computer Science & Hugh Kaul Precision Medicine Institute University of Alabama at Birmingham Tutorial Title: Relational Programming in miniKanren: an Interactive Tutorial Abstract: Relational Programming is a paradigm in which programs represent mathematical relations (in contrast to functional programming, in which programs represent mathematical functions). Unlike traditional programs, relational programs do not distinguish between inputs and outputs. Instead, *any* argument to a relational program can be treated as either an input or an output. This unusual property makes relational programs extremely flexible, and able to automatically perform tasks that would be complicated to implement using standard techniques. For example, an interpreter written as a relation is able to perform *program synthesis*, automatically generating programs from input/output examples. In this in-depth, interactive, two day tutorial, we will explore the world of relational programming using miniKanren, a language specifically designed for writing interesting programs as relations. Together we will implement the core of the miniKanren relational programming language. We will also implement an interpreter for a subset of Racket, written as a miniKanren relation. We will then use this "relational interpreter" to perform simple program synthesis, and discuss techniques that can speed up synthesis by many orders of magnitude. The tutorial will be highly interactive. We will implement all the code together, using the Racket programming language (a variant of Scheme). We will begin with a short introduction to basics of the Racket language, which can be learned in a few minutes. If you would like to implement all the code yourself, please bring a laptop with DrRacket installed (https://racket-lang.org/). If you don't want to implement the code yourself, you can participate by helping me as I write the code at the projector! :) Topics we will cover in the tutorial: * fundamental concepts of relational programming * a brief introduction to the Racket programming language * introduction to the miniKanren relational programming language * writing recursive relations in miniKanren * writing a simple Racket interpreter as a function in Racket * writing a simple Racket interpreter as a relation in miniKanren * using the relational Racket interpreter to perform simple program synthesis * optimizations and extensions to the relational Racket interpreter * implementing the core of miniKanren (microKanren) * open research problems in relational programming * lots of other interesting related topics -- 五十嵐淳 (IGARASHI Atsushi) E-mail: igarashi(a)kuis.kyoto-u.ac.jp url: http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/

1 0

Talk by Soichiro Fujii (10 May, 11.00-, at Kyoto University)
by Kazushige TERUI 06 May '18

06 May '18

皆様今週木曜日に、京都大学にて藤井宗一郎さんのご講演があります。詳細は以下のとおりです。どうぞお気軽にご参加ください。京都大学数理解析研究所照井一成 ==================== Time: 11:00-12:00, 10 May, 2018 Place: Rm 478, Research Building 2, Main Campus, Kyoto University 京都大学本部構内総合研究2号館 4階478号室 http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (Building 34) Speaker: 藤井宗一郎 Soichiro Fujii (U Tokyo) Title: A unified framework for notions of algebraic theory Abstract: Universal algebra uniformly captures various algebraic structures, by expressing them as equational theories or (abstract) clones. The ubiquity of algebraic structures in mathematics has also given rise to several variants of universal algebra, such as symmetric and non-symmetric operads, clubs, and monads. In this talk, I will present a unified framework for these cousins of universal algebra, or notions of algebraic theory. First I will explain how each notion of algebraic theory can be identified with a certain monoidal category, in such a way that theories correspond to monoids. Then I will introduce a categorical structure underlying the definition of models of theories. In specific examples, it often arises in the form of oplax action or enrichment. Finally I will uniformly characterize categories of models for various notions of algebraic theory, by a double-categorical universal property in the pseudo-double category of profunctors.

1 0

Project colloquium talk by Paolo Arcaini on 9 May
by urabenatsuki＠is.s.u-tokyo.ac.jp 05 May '18

05 May '18

[Apologies for multiple copies] Dear all, Let me advertise our next ERATO MMSD project colloquium talk by Paolo Arcaini on 9th May, 16:30-. Please find the title and the abstract below. You are all invited. Sincerely, -- Natsuki Urabe urabenatsuki(a)is.s.u-tokyo.ac.jp The University of Tokyo, ERATO MMSD ----- Wed 9 May 2018, 16:30–18:00 ERATO MMSD Takebashi Site Common Room 3 http://group-mmm.org/eratommsd/access.html Paolo Arcaini (National Institute of Informatics <http://www.nii.ac.jp/>), Decomposition-Based Approach for Model-Based Test Generation Model-based test generation by model checking is a well-known testing technique that, however, suffers from the state explosion problem of model checking and it is, therefore, not always applicable. In this talk, I present an approach that addresses this issue by decomposing a system model into suitable subsystem models separately analyzable. The technique consists in decomposing that portion of a system model that is of interest for a given testing requirement, into a tree of subsystems by exploiting information on model variable dependency. The technique generates tests for the whole system model by merging tests built from those subsystems. Effectiveness and efficiency of the proposed decomposition-based test generation approach are measured both in terms of coverage and time.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml May 2018