diff --git a/content/lsd-seminar/2024fa.md b/content/lsd-seminar/2024fa.md index 1dbb5a0..30a7231 100644 --- a/content/lsd-seminar/2024fa.md +++ b/content/lsd-seminar/2024fa.md @@ -20,7 +20,7 @@ Talks will be advertised on the [ucsc-lsd-seminar-announce](https://groups.googl | Date | Speaker | Title | |------- |--------- |--------- | | [Oct 4](#oct-4) | Jinsheng Ba | Testing Database Engines via Query Plans | -| [Oct 11](#oct-11) | Jonathan Castello | _TBD_ | +| [Oct 11](#oct-11) | Jonathan Castello | Inductive diagrams for causal reasoning | | [Oct 18](#oct-18) | Bastian Köpcke | _TBD_ | | [Oct 25](#oct-25) | Haofan Zheng | _TBD_ | | [Nov 1](#nov-1) | Justin Lubin | _TBD_ | @@ -45,11 +45,11 @@ Talks will be advertised on the [ucsc-lsd-seminar-announce](https://groups.googl **Speaker:** Jonathan Castello -**Title:** _TBD_ +**Title:** Inductive diagrams for causal reasoning -**Abstract:** _TBD_ +**Abstract:** Causality diagrams are used throughout academia and industry to informally reason about the possible executions of distributed and concurrent systems. Their formal counterparts, what we'll call Lamport executions, have been used since at least Lamport's 1978 introduction of logical clocks. However, Lamport executions are not quite as visceral a model for humans as causality diagrams. This mismatch is exacerbated in modern proof assistants, which are geared toward *compositional reasoning* over inductive data. In this talk, we'll present a new formal representation of executions that is both inductively-structured and more similar to the informal diagrams we started with. -**Bio:** _TBD_ +**Bio:** Jonathan is a third-year Ph.D. student at UC Santa Cruz. His research focuses on treating concurrency as something to be started from, rather than something to be introduced to an existing system. This perspective leads to interests in distributed systems, network protocols, and low-level hardware, among other threads(!). In his spare time, he nurtures a continued fascination with all things space. ## Oct 18