Department of

# Mathematics

Seminar Calendar
for events the day of Friday, November 3, 2017.

.
events for the
events containing

Questions regarding events or the calendar should be directed to Tori Corkery.
     October 2017          November 2017          December 2017
Su Mo Tu We Th Fr Sa   Su Mo Tu We Th Fr Sa   Su Mo Tu We Th Fr Sa
1  2  3  4  5  6  7             1  2  3  4                   1  2
8  9 10 11 12 13 14    5  6  7  8  9 10 11    3  4  5  6  7  8  9
15 16 17 18 19 20 21   12 13 14 15 16 17 18   10 11 12 13 14 15 16
22 23 24 25 26 27 28   19 20 21 22 23 24 25   17 18 19 20 21 22 23
29 30 31               26 27 28 29 30         24 25 26 27 28 29 30
31


Friday, November 3, 2017

12:00 pm in 245 Altgeld Hall,Friday, November 3, 2017

#### Scattered Results on the Bishop-Phelps-Bollobás Property

###### Kimberly Duran (UIUC)

Abstract: The Bishop-Phelps-Bollobás property for a space of operators is a stronger version of having a dense subset of norm-attaining operators. This is a topic in functional analysis with a many scattered results, and as yet few large unifying problems. I'll discuss the historical development and some of the known positive and negative results in this expository talk.

2:00 pm in 3403 Siebel ,Friday, November 3, 2017

#### Verifiable C, a logic and tool for deductive verification of the correctness of C programs

###### Andrew W. Appel (Eugene Higgins Professor of Computer Science, Princeton University)

Abstract: What do we need in a practical program logic and tool for verifying C programs? It must support pointer data structures with sharing and mutation: separation logic is useful. It should facilitate the use of function pointers in such usage patterns as “objects” or “closures”: it should be higher-order. It should support data abstraction, especially in connection with objects and closures; that is, quantification over representation predicates. Each program is verified in its own application domain, so the program logic should have strong facilities and libraries for reasoning in the mathematics of many application domains. So the program logic be embedded in a general-purpose logic and proof assistant such as Coq. Verifiable C is a higher-order concurrent separation logic for C, embedded in Coq, as part of the Verified Software Toolchain. It is proved sound with a machine-checked proof in Coq. It assists users in interactively building correctness proofs for their C programs. In this talk I will explain the requirements, design, implementation, and practical use of the Verified Software Toolchain. (Sponsored by the Department of Computer Science)

Bio: Andrew W. Appel is Eugene Higgins Professor of Computer Science at Princeton University, where he has been on the faculty since 1986. He served as Department Chair from 2009-2015. His research is in software verification, computer security, programming languages and compilers, and technology policy. He received his A.B. summa cum laude in physics from Princeton in 1981, and his PhD in computer science from Carnegie Mellon University in 1985. He has been Editor in Chief of ACM Transactions on Programming Languages and Systems and is a Fellow of the ACM (Association for Computing Machinery). He has worked on fast N-body algorithms (1980s), Standard ML of New Jersey (1990s), Foundational Proof-Carrying Code (2000s), and the Verified Software Toolchain (2010s).

3:00 pm in 341 Altgeld Hall,Friday, November 3, 2017

#### On the Gorensteinization of Schubert varieties via boundary divisors

###### Sergio Da Silva (Cornell University)

Abstract: A variety being Gorenstein can be a useful property to have when considering questions in birational geometry. Although Schubert varieties are Cohen-Macaulay, they are not Gorenstein in general. I will describe a convenient way to find a "Gorensteinization" for a Schubert variety by considering only one blow-up along its boundary divisor. We start by reducing to the local question, one involving Kazhdan-Lusztig varieties. These affine varieties can be degenerated to a toric variety defined using the Stanley-Reisner ideal of a subword complex. The blow-up of this variety along its boundary is now Gorenstein. Carefully choosing a degeneration of the blow-up allows us to extend this result to Schubert varieties.

4:00 pm in 345 Altgeld Hall,Friday, November 3, 2017

#### Cancelled

4:00 pm in Knight Auditorium, Spurlock Museum; followed by reception, 5pm-7pm, Ballroom, Alice Campbell Alumni Center,Friday, November 3, 2017

#### Graph coloring and machine proofs in computer science, 1977-2017

###### Andrew W. Appel (Eugene Higgins Professor of Computer Science, Princeton University)

Abstract: The Four Color Theorem of Kenneth Appel and Wolfgang Haken (1976) was proved and checked with the assistance of computer programs, though much of the proof was written (and refereed) only by humans. Contemporaneously, Edinburgh LCF (Logic for Computable Functions) was developed by Robin Milner--a system for proofs written by humans (with computer assistance) but completely checked by computer; with particular application to proofs about computer programs. These two developments, and their convergence, have had significant impact on computer science, and my own research career: graph-coloring algorithms for register allocation in compilers, functional programming languages, fully machine-checked proofs of mathematical theorems, fully machine-checked proofs of software systems. One result at the intersection of all these is a machine-checked proof of correctness of a program that does register allocation by graph-coloring, using an algorithm related to one used in every four-color proof (and attempted proof) since 1879.

4:00 pm in 241 Altgeld Hall,Friday, November 3, 2017