Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| seminars [2024-09-25] – [Implementation of the Burau spectral test] Martin Ziegler | seminars [2025-12-05] (current) – [Computing with the Millett-Ewing notation] 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# | ||
| * [[Seminars# | * [[Seminars# | ||
| * [[Seminars# | * [[Seminars# | ||
| Line 11: | Line 12: | ||
| * [[Seminars# | * [[Seminars# | ||
| * [[Seminars# | * [[Seminars# | ||
| + | |||
| + | ===== 2025 ===== | ||
| + | |||
| + | ====Computing with the Millett-Ewing notation==== | ||
| + | * December 12, time TBD | ||
| + | * N1 #422 or #110 | ||
| + | * Alexander Stoimenov (Dongguk U) | ||
| + | |||
| + | This talk gives some introduction about the notation of link diagrams developed by Millett-Ewing in the late 80s for calculating link polynomials. | ||
| + | I explain how this notation is used by Knotscape (for this see [[https:// | ||
| + | before giving some details on the Millett-Ewing algorithm and (my) several subsequent modifications and extensions. | ||
| + | |||
| + | ====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' | ||
| + | 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' | ||
| + | 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, | ||
| + | verification, | ||
| + | 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, | ||
| + | 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 ===== | ||
| ====iRRAM for Knots==== | ====iRRAM for Knots==== | ||
| - | * September 26, 11h00 KST | + | |
| - | * hybrid offline (N1 #524) + online (Zoom, ask for coordinates) | + | * hybrid offline (N1 #524) + online (Zoom, ask for coordinates) |
| - | * Jaden Jorradol (KAIST) | + | * Jaden Jorradol (KAIST) |
| Rehearsal for presentation of [[https:// | Rehearsal for presentation of [[https:// | ||