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-06-05] – [Faster multiplication on small numbers with FPU] Svetlana Selivanovaseminars [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====
 +  * [[http://youtu.be/8Ke8XhtPzQE|Nov 6, 17h00]], via Zoom 
 +  * Jiman Hwang (KAIST)
 +
 +Abstract: Representing a compact set C ⊂ ℝⁿ is equivalent to defining a characteristic function f:ℝⁿ->{0,1} where f(x)=1 if x ∈ C and f(x)=0 otherwise. When it comes to implementation, however, f is not decidable on the boundary. One solution is to make the characteristic function multivalued allowing overlap around the boundary with precision parameter p. For instance, define f:ℝⁿ×ℕ->{0,1} that produces 1 if B(x,2⁻ᴾ⁺¹)∩C≠∅ and 0 if B(x,2⁻ᴾ)∩C=∅ where B(x,r) is the open ball centered at x with radius r. In this talk we show 1) how to plot an image of a compact set given a characteristic function and 2) how to create a characteristic function corresponding to a compact set that covers given g:[0,1]ᵐ->ℝⁿ.
 +
 +====Computability of Probability measure and Random sampling====
 +  * Sep 18, 11h00, via Zoom 
 +  * Hyunwoo Lee (KAIST)
 +
 +Abstract: The computability of Probability measure has many different definition. Like sampling or valuation. Unfortunately, not all of them are equivalent.  In this talk, I'll explain the definition of different kinds of computability of measures, and relation between them.  From this relation, I suggest the notion of complexity of probability measure, namely sampling complexity and expectation complexity.
 +
 +
 +====Introduction to Knot Theory for Computer Scientists====
 +  * [[http://youtu.be/jSn3OjBA3R8|Sept. 14, 14h00]], via Zoom 
 +  * Alexander Stoimenov
 +
 +Abstract: Knot theory is a popular topic in Topology/Pure Mathematics. 
 +This is an introductory talk to knot theory at the level for graduate students of computer science. The goal is to explain knots, and how to understand them in terms suitable for computing (diagrams and the DT code), what are link polynomials and braids (and the Burau representation). At the end I plan to introduce the program [[https://github.com/dimpase/knotscap|KnotScape]] and explain how it can be used (or not) to draw knots and do various calculations with them.
 +
 ====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 algorthms, 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.+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 24: Line 150:
  
 ==== Complexity of raising small polynomials with real coefficients to exponential power ==== ==== Complexity of raising small polynomials with real coefficients to exponential power ====
-  * 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 33: 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 49: 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 69: 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 82: 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 91: 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 98: 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 111: 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 124: 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)
      
Line 261: Line 387:
  
 ====  Grassmannian as Continuous Abstract Data Type with Computable Semantics  ==== ====  Grassmannian as Continuous Abstract Data Type with Computable Semantics  ====
-  * Sep 30, 15h30, E3-1 #3420+  * [[http://youtu.be/2eMmS7GSiIo|Sep 30, 15h30]], E3-1 #3420
   * Seokbin Lee (KAIST)   * Seokbin Lee (KAIST)