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 [2024-09-25] – [iRRAM for Knots] Martin Zieglerseminars [2025-08-13] (current) – [XpLUTo: Modelling Bulk Parallel Processing in RAM via Lookup Tables] 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#2025]]  
   * [[Seminars#2024]]     * [[Seminars#2024]]  
   * [[Seminars#2023]]   * [[Seminars#2023]]
Line 11: Line 12:
   * [[Seminars#2016]]   * [[Seminars#2016]]
   * [[Seminars#2015]]   * [[Seminars#2015]]
 +
 +===== 2025 =====
 +
 +====XpLUTo: Modelling Bulk Parallel Processing in RAM via Lookup Tables====
 +  * August 12, 4pm KST
 +  * E3-1 #4420 and online
 +  * Nguyên Trần Bảo (HCMUT and KAIST)
 +
 +Processing-in-memory (PIM) has been investigated for its ability to
 +perform bulk data operations while eliminating data movement, which is a major
 +performance bottleneck. However, existing designs, regardless of how minimal,
 +still require modifications to the physical memory circuitry. Moreover, each
 +proposed operation introduces different primitives, inherently hindering the development
 +of a general design capable of supporting all operations. In this work,
 +we propose XPLUTO, a new parallel architecture model that leverages the capabilities
 +of PIM. Our key observation is that, in the worst case, any complex
 +operation can be implemented via a lookup table (precomputation and query),
 +which can be viewed as a SIMD (single-instruction multiple-data) operation.
 +Based on this insight, we focus on designing algorithms built upon SIMD operations,
 +with asymptotic costs estimated according to lookup table performance.
 +So far, XPLUTO has demonstrated the ability to emulate various problems,
 +including sorting, addition, and prefix operations.
 +
 +
 +====Integer factorization of matrices and 4-dimensional genera of knots====
 +  * March 19, 9:15am KST 
 +  * N1 #601
 +  * Alexander Stoimenov (Dongguk U)
 +
 +This is a lecture, in which I explain
 +the methods for computing (smooth) 4-dimensional genera of knots,
 +based on signatures
 +and Donaldson's theorem, which leads to a criterion for the
 +integer factorization of Goeritz matrices. Here I will talk
 +about how to efficiently implement the search for such
 +factorizations.
 +I plan to show Chuck Livingston's KnotInfo site, and his notes on
 +my contributions to the computation of (smooth) 4-dimensional genera.
 +
 +====Automated Reasoning with Continuous Data====
 +  * March 19, 10:00am KST
 +  * N1 #601
 +  * Margarita Korovina (IIS SB RAS)
 +
 +In this talk we report on ongoing research on solving non-linear constraints
 +over the reals occurring in a wide range of applications, starting with program
 +verification, ranging over verification of real-world designs all the way to automation
 +of formally verified proofs of mathematical statements. In our framework
 +methods from Computable Analysis and Automated Reasoning are combined to
 +meet efficiency and expressiveness. This approach is applicable to a large number
 +of constraints involving computable non-linear functions, piecewise polynomial
 +splines, transcendental functions and solutions of polynomial differential equations.
 +We give an introduction to the **ksmt** calculus for checking satisfiability of
 +non-linear constraints in a CDCL style way inspired by advances in SAT solving.
 +Along proof search **ksmt** resolves two types of conflicts: linear and non-linear.
 +Linear conflicts are delegated to a decision procedure for linear real arithmetic
 +and non-linear conflicts are resolved by local linearisations separating the solution
 +set and the current conflict. We show that the ksmt calculus is a δ-complete
 +decision procedure for bounded problems. In this setting we discuss resent and
 +future research work.
 +
 +====From iRRAM to pyRRAM: Some thoughts on implementing real number arithmetic====
 +  * March 19, 10:45am KST  
 +  * N1 #601
 +  * Norbert Müller (Uni Trier)
 +
 +Due to their uncountability, real numbers have to be treated
 +completely
 +different compared to countable sets like the integer or even the
 +rational
 +numbers. In the talk we present basic ideas for implementations in
 +an existing
 +library written in C++ and in a derived current approach in
 +Python.
 +
  
 ===== 2024 ===== ===== 2024 =====