Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
seminars [2020-11-06] – [Grassmannian as Continuous Abstract Data Type with Computable Semantics] Martin Zieglerseminars [2023-06-28] (current) – 2023 Martin Ziegler
Line 1: Line 1:
 ====== Seminar on Theoretical Computer Science, Logic, and Real Computation ====== ====== Seminar on Theoretical Computer Science, Logic, and Real Computation ======
  
 +  * [[Seminars#2023]] 
 +  * [[Seminars#2022]] 
 +  * [[Seminars#2021]] 
 +  * [[Seminars#2020]]
   * [[Seminars#2019]]   * [[Seminars#2019]]
   * [[Seminars#2018]]   * [[Seminars#2018]]
Line 7: Line 10:
   * [[Seminars#2016]]   * [[Seminars#2016]]
   * [[Seminars#2015]]   * [[Seminars#2015]]
 +
 +===== 2023 =====
 +
 +* June 28, 19h KST
 +* Rakhman Ulzhalgas (KAIST) 
 +
 +"//Continuous Local Strategies for Robotic Formation Problems//"
 +by Barbara Kempkes and Friedhelm Meyer auf der Heide (2012)
 +
 +===== 2022 =====
 +
 +====Computing with Infinite Objects via Coinductive Definitions====
 +  * June 2, 14h30 KST
 +  * Dieter Spreen (U Siegen)
 +
 +//Abstract://
 +A representation-free logic-base approach for computing with infinite objects will be presented. The logic is intuitionistic first-order logic extended by strictly positive inductive and coinductive definitions. Algorithms can be extracted from proofs via realizability. The approach allows to deal with objects like the real numbers and nonempty compact sets of such. More general, it allows to deal with compact metric spaces that come equipped with a finite set of contractions such that the union of their ranges covers the space, and with continuous maps between such spaces. The computational power of the approach is equivalent to that of type-two theory of effectivity.
 +
 +{{http://kaist.theoryofcomputation.asia/_media/screenshot_2022-06-02_152534.png}}
 +===== 2021 =====
 +
 +
 +
 +====Book Review "Governing the Commons" by Elinor Ostrom====
 +  * July 9, 16h00, via Zoom 
 +  * Lwam Z. Araya (KAIST)
 +
 +Abstract: 
 +//Governing the Commons: The Evolution of Institutions for Collective Action// is an examination of the nature of the commons, and the evolution and development of self-organisation and self-governance of those commons. //The Evolution of Institutions for Collective Action// will be of interest to those who seek an understanding of common-pool resources and their self-governance. I am going to present chapter one of the book. Chapter one begins with an examination of the commons and the presentation of three models of the commons. Professor Elinor Ostrom discusses: the tragedy of the commons, the prisoner's dilemma game, and the logic of collective action. Then the Professor concludes with comparison of the Leviathan approach and the privatization approach to the governance of the commons. To these two approaches the professor offers an empirical alternative. I will recommend the book to every human being. It is an interesting and inspiring book. I am looking forward to see you on the meetin
 +
 +====Lazy types in iRRAM and computability of Mandelbrot set====
 +  * May 6, 16h00, via Zoom 
 +  * Jihoon Hyun (KAIST)
 +
 +Abstract: iRRAM iterates all over if more precision is needed. In other words, iRRAM iterates all over even if only a few parts of the program need extra precision. And if that expensively-calculated expression is actually not used in the program, for example by the use of choose function, it will be a waste of computational resources. Although iRRAM has implemented LAZY_BOOLEAN, we need more laziness to remove that kind of computation. So Sewon introduced the lazy versions of types of iRRAM. I will discuss how I could implement the lazy type with iRRAM. I will also discuss briefly about lazy evaluation using call-by-need with iRRAM.
 +
 +Mandelbrot set is a set of complex numbers whose exterior is computably enumerable. There is a conjecture which says that the Mandelbrot set is also computably enumerable. I will mention some facts about the set, and explain what I have done with iRRAM to draw the set on a plane.
 +
 +====Introduction to mathematical Ludology====
 +  * Apr 29, 16h00, via Zoom 
 +  * Hyunwoo Lee (KAIST)
 +
 +Abstract: Game is a part of human life from ancient times. However, there were only a few attempts to study games using mathematics. Although there is the academic field called game theory, the notion of the game in game theory is a bit different from the game which we really play in regular life. Another attempt is using narratology, which studies the game as storytelling media. However, unlike a  movie or a novel, storytelling is not the main property of a game. Actually, most gamers are concentrated on 'playing', more than storytelling.
 +In this talk, I introduce a young academic discipline called Ludology, especially mathematical Ludology which studies and analyzes the game 'playing' using mathematics and computer science. In this area, the formal description of a game is regarded as  a mathematical model which satisfies the rules of the game. I will talk about GDL formalism, its applications, the limitations of GDL and other attempts to formalize a game.
 +
 +====Introduction to Riemannian Geometry, Part IV and V====
 +  * Apr 1, 16h00, via Zoom 
 +  * Apr 22, 16h00, via Zoom (continued)
 +  * Filippo Morabito (KAIST)
 +
 +Abstract: During this talk I will present some elements of analysis of the singularities 
 +of the Ricci flow.
 +
 +====Introduction to Riemannian Geometry, Part III====
 +  * Mar 19, 14h00, via Zoom
 +  * Filippo Morabito (KAIST)
 +
 +Abstract: In this lecture I will present the notions of covariant derivative, Riemann curvature 
 +tensor and Ricci tensor.
 +
 +====Introduction to Computable Analysis====
 +  * Mar 11, 16h00, via Zoom 
 +  * Hyunwoo Lee (KAIST)
 +
 +Abstract: This is a brief and not very rigorous talk about basics of computable analysis.  I will cover the concept of a computable number, sequence, function and related results.
 +If time allows, I will also explain the concept of a computable manifold I'm recently working on.
 +
 +====Introduction to Riemannian Geometry, Part II====
 +  * Mar 4, 16h00, via Zoom
 +  * Filippo Morabito (KAIST)
 +
 +Abstract: In this second talk I will introduce the notion of tensor
 + and I will present some examples of Riemannian manifold.
 +
 +====Introduction to Riemannian Geometry, Part I====
 +  * Feb 25, 16h00, via Zoom
 +  * Filippo Morabito (KAIST)
 +
 +Abstract: This talk is the first of a series of talks which aim to present
 +the main results concerning a powerful analytic method for studying 
 +the geometry and the topology of manifolds, the Ricci flow. During this 
 +first talk I will provide the audience with the notions of Riemannian 
 +geometry which are necessary for understanding the Ricci flow.
 +
 +
  
 ===== 2020 ===== ===== 2020 =====
 +
 +
 +
 +====Applications of type theory in imperative programming languages====
 +  * Nov 19, 18h30, via Zoom
 +  * Gyesik Lee (Hankyong National University)
 +
 +Abstract: For decades the study of type systems for programming languages has been one of the most active areas of computer science research, with important applications in software engineering, programming language design, high performance compiler implementation, and security of information networks. This talk aims to introduce the area and will cover some range and applications of related topics from type theory including simple/polymorphic type systems, subtyping, and recursive types.
 +
 +====Knotscape and Knot Tables====
 +  * Nov 12, 18h30, via Zoom 
 +  * Alexander Stoimenov (KAIST)
 +
 +Abstract: After some brief review of basic concepts from the first lecture,
 +I will give an introduction to the table access program
 +Knotscape and its basic features, focusing primarily on its
 +knot location tool.
 +
 ====Visualization of a compact set ⊂ ℝⁿ in Exact Real Computation==== ====Visualization of a compact set ⊂ ℝⁿ in Exact Real Computation====
-  * [[http://youtu.be/8Ke8XhtPzQE|Nov 6, 17h00]], via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * [[http://youtu.be/8Ke8XhtPzQE|Nov 6, 17h00]], via Zoom 
   * Jiman Hwang (KAIST)   * Jiman Hwang (KAIST)
  
Line 16: Line 122:
  
 ====Computability of Probability measure and Random sampling==== ====Computability of Probability measure and Random sampling====
-  * Sep 18, 11h00, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * Sep 18, 11h00, via Zoom 
   * Hyunwoo Lee (KAIST)   * Hyunwoo Lee (KAIST)
  
Line 23: Line 129:
  
 ====Introduction to Knot Theory for Computer Scientists==== ====Introduction to Knot Theory for Computer Scientists====
-  * Sept. 14, 14h00, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * [[http://youtu.be/jSn3OjBA3R8|Sept. 14, 14h00]], via Zoom 
   * Alexander Stoimenov   * Alexander Stoimenov
  
Line 30: Line 136:
  
 ====Computable conditional distribution==== ====Computable conditional distribution====
-  * June 10, 16h30, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * June 10, 16h30, via Zoom 
   * Hyunwoo Lee (KAIST)   * Hyunwoo Lee (KAIST)
  
 Abstract: In the area of machine learning or statistical inference algorithms, conditional distribution plays the main role. For discrete random variables, computing the conditional distribution is quite intuitive, and there's no problem to define computability of such a distribution. However, for the continuous case, it's not an easy problem. Let's consider the following situation. Let X and Y be dependent random variable with uniform distribution on [0,1]. Then what is the value of P(0<X<0.5|Y=1)? With  the classical definition, we can not say anything about its value, even though such probability is meaningful. Abstract: In the area of machine learning or statistical inference algorithms, conditional distribution plays the main role. For discrete random variables, computing the conditional distribution is quite intuitive, and there's no problem to define computability of such a distribution. However, for the continuous case, it's not an easy problem. Let's consider the following situation. Let X and Y be dependent random variable with uniform distribution on [0,1]. Then what is the value of P(0<X<0.5|Y=1)? With  the classical definition, we can not say anything about its value, even though such probability is meaningful.
 In this talk, I'll introduce the extended definition of a conditional distribution using the concept of probability kernel, and also define the Type-2 computability of it. Also, I'll show that there exists a conditional distribution which is not computable. Finally, some known results about computability of conditional distributions will be discussed. (This talk is based on the paper  "Noncomputable conditional distributions." by Ackerman et al.) In this talk, I'll introduce the extended definition of a conditional distribution using the concept of probability kernel, and also define the Type-2 computability of it. Also, I'll show that there exists a conditional distribution which is not computable. Finally, some known results about computability of conditional distributions will be discussed. (This talk is based on the paper  "Noncomputable conditional distributions." by Ackerman et al.)
 +
 ====Faster multiplication on small numbers with FPU ==== ====Faster multiplication on small numbers with FPU ====
-  * June 4, 16h30, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * June 4, 16h30, via Zoom
   * Jiman Hwang (KAIST)   * Jiman Hwang (KAIST)
  
Line 43: Line 150:
  
 ==== Complexity of raising small polynomials with real coefficients to exponential power ==== ==== Complexity of raising small polynomials with real coefficients to exponential power ====
-  * [[http://youtu.be/xMjcXg9SCzA|May 29, 17h05]], via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * [[http://youtu.be/xMjcXg9SCzA|May 29, 17h05]], via Zoom
   * Ivan Adrian Koswara (KAIST)   * Ivan Adrian Koswara (KAIST)
  
Line 52: Line 159:
 ==== Classical Types in a Constructive Type Theory and a Transfer Principle for Classical Proofs ==== ==== Classical Types in a Constructive Type Theory and a Transfer Principle for Classical Proofs ====
  
-  * May 21, 16h30, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * May 21, 16h30, via Zoom 
   * Sewon Park (KAIST)   * Sewon Park (KAIST)
  
Line 68: Line 175:
  
 ==== Rigorous Numerical Computing with ARIADNE ==== ==== Rigorous Numerical Computing with ARIADNE ====
-  * May 14, 16h30, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * May 14, 16h30, via Zoom 
   * Pieter Collins (Maastricht University)   * Pieter Collins (Maastricht University)
  
Line 88: Line 195:
  
 ==== Computational complexity and practice of analytic ODE solving ==== ==== Computational complexity and practice of analytic ODE solving ====
-  * May 7, 16h30, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * May 7, 16h30, via Zoom 
   * Holger Thies (Kyushu University)   * Holger Thies (Kyushu University)
  
Line 101: Line 208:
  
 ==== Implementation of Computable Real Numbers in Haskell ==== ==== Implementation of Computable Real Numbers in Haskell ====
-  * May 1, 17h00, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * May 1, 17h00, via Zoom 
   * Shinhwan Park (Korea University)   * Shinhwan Park (Korea University)
  
Line 110: Line 217:
  
 ==== Continuity of Multivalued Functions ==== ==== Continuity of Multivalued Functions ====
-  * April 24, 17h00, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * April 24, 17h00, via Zoom 
   * Donghyun Lim (KAIST)   * Donghyun Lim (KAIST)
  
Line 117: Line 224:
  
 ==== Avoiding search and extracting function names ==== ==== Avoiding search and extracting function names ====
-  * April 16, 17h00, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#dr_svetlana_selivanova|Svetlana]] for the link)+  * April 16, 17h00, via Zoom 
   * Florian Steinberg    * Florian Steinberg 
  
Line 130: Line 237:
  
 ==== Verified and efficient exact real computation in Coq ==== ==== Verified and efficient exact real computation in Coq ====
-  * April 9, 17h00, via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#sewon_park|Sewon]] for the link)+  * April 9, 17h00, via Zoom
   * Holger Thies (Kyushu University)   * Holger Thies (Kyushu University)
  
Line 143: Line 250:
  
 ==== Representations for Product Spaces ==== ==== Representations for Product Spaces ====
-  * 2020, April 3, 17:00 (UTC+9), via Zoom (contact [[https://kaist.theoryofcomputation.asia/members#sewon_park|Sewon]] for the link)+  * 2020, April 3, 17:00 (UTC+9), via Zoom 
   * Donghyun Lim (KAIST)   * Donghyun Lim (KAIST)