Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
| seminars [2022-05-29] – [2022] New Martin Ziegler | seminars [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# | ||
| + | * [[Seminars# | ||
| * [[Seminars# | * [[Seminars# | ||
| * [[Seminars# | * [[Seminars# | ||
| Line 9: | Line 11: | ||
| * [[Seminars# | * [[Seminars# | ||
| - | ===== 2022 ===== | + | ===== 2023 ===== |
| + | * June 28, 19h KST | ||
| + | * Rakhman Ulzhalgas (KAIST) | ||
| + | |||
| + | "// | ||
| + | by Barbara Kempkes and Friedhelm Meyer auf der Heide (2012) | ||
| + | |||
| + | ===== 2022 ===== | ||
| ====Computing with Infinite Objects via Coinductive Definitions==== | ====Computing with Infinite Objects via Coinductive Definitions==== | ||
| Line 16: | Line 25: | ||
| * Dieter Spreen (U Siegen) | * Dieter Spreen (U Siegen) | ||
| - | Abstract: | + | //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.// | + | 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:// | ||
| ===== 2021 ===== | ===== 2021 ===== | ||