[TYPES/announce] Nordic Online Logic Seminar: next talk on Monday, 18 December by Göran Sundholm
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Nordic Online Logic Seminar (NOL Seminar) is organised monthly over Zoom, with expository talks on topics of interest for the broader logic community. The seminar is open for professional or aspiring logicians and logic aficionados worldwide. See the announcement for the next talk below. If you wish to receive the Zoom ID and password for it, as well as further announcements, please subscribe here: https://urldefense.com/v3/__https://listserv.gu.se/sympa/subscribe/nordiclogic__;!!IBzWLUs!TxzFxNGscG-WvBTStbsyOSXM7A0C2MckruxZNnt8K8rFNqJCk2fPt8dcnl354_fSreP9ZPxQ2wXVzmQSrokzP0ebQDINl06DzfM$ . Val Goranko and Graham Leigh NOL seminar organisers Nordic Online Logic Seminar Date Monday, 18 December 2023 at 16:00 CET (UTC+1) on Zoom Speaker Göran Sundholm (Professor of Logic (em.), Leiden University) Title Curry-Howard: a meaning explanation or just another realizability interpretation? Abstract Around 1930 a major paradigm shift occurred in the foundations of mathematics; we may call it the METAMATHEMATICAL TURN. Until then the task of a logician had been to design and explain a full-scale formal language that was adequate for the practice of mathematical analysis in such a way that the axioms and rules of inference of the theory were rendered evident by the explanations. The metamathematical turn changed the status of the formal languages: now they became (meta)mathematical objects of study. We no longer communicate with the aid of the formal systems – we communicate about them. Kleene’s realizability (JSL 1945) gave a metamathematical (re-)interpretation of arithmetic inside arithmetic. Heyting and Kolmogorov (1931-2), on the other hand, had used “proofs” of propositions, respectively “solutions” to problems, in order to explain the meaning of the mathematical language, rather than reinterpret it internally. We now have the choice to view the Curry-Howard isomorphism, say, as a variant of realizability, when it will be an internal mathematical re-interpretation, or to adopt an atavistic, Frege-like, viewpoint and look at the language as being rendered meaningful. This perspective will be used to discuss another paradigm shift, namely that of distinguishing constructivism and intuitionism. The hesitant attitude of Gödel, Kreisel, and Michael Dummett, will be spelled out, and, at the hand of unpublished source material, a likely reason given.
[TYPES/announce] Funded PhD Positions at Boston University
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Hi all, I am excited to announce that I will be joining Boston University as a tenure-track assistant professor in the Computer Science department. Also, the Boston University Programming Languages and Verification group (POPV) is looking for PhD students. https://urldefense.com/v3/__http://www.bu.edu/cs/research/popv/__;!!IBzWLUs!TtM6s20yDRt4JyDD6uRd8hJPGTwq3dv5LY3iAyqibDhD-RLyClgr18XWmHKEDkwBymh82zZ6XTWa1zS5-PxssUzk6h_SyNkn9DN-$ The group consists of several faculty, postdocs and students with interests in different aspects of programming languages, verification, type theories and proof assistants. Members of the POPV group actively collaborate with other groups at Boston University, including the Boston University Security group ( https://urldefense.com/v3/__https://www.bu.edu/cs/groups/busec/__;!!IBzWLUs!TtM6s20yDRt4JyDD6uRd8hJPGTwq3dv5LY3iAyqibDhD-RLyClgr18XWmHKEDkwBymh82zZ6XTWa1zS5-PxssUzk6h_SyPYMGYgx$ ), and at other universities in the Boston area. Interested candidates are encouraged to contact me or one of the other faculty in the group. The deadline for applications is December 15, 2023. The official application information can be found here: https://urldefense.com/v3/__https://www.bu.edu/cs/phd-program/phd/__;!!IBzWLUs!TtM6s20yDRt4JyDD6uRd8hJPGTwq3dv5LY3iAyqibDhD-RLyClgr18XWmHKEDkwBymh82zZ6XTWa1zS5-PxssUzk6h_SyE09l5nr$ Application fees can be waived, if needed. More details here: https://urldefense.com/v3/__https://www.bu.edu/cs/phd-program/phd/faqs-about-graduate-admissions-financial-aid/__;!!IBzWLUs!TtM6s20yDRt4JyDD6uRd8hJPGTwq3dv5LY3iAyqibDhD-RLyClgr18XWmHKEDkwBymh82zZ6XTWa1zS5-PxssUzk6h_SyBLTmxRA$ All admitted PhD students will receive a 5-year fellowship offer, which may be a combination of a non-service fellowship, teaching fellowship or doctoral research assistant. Boston University is a large private University on the west side of Boston with a rich tradition of inclusion and social justice. We are proud that we were the first American university to award a PhD to a woman (1877) and that Martin Luther King Jr. received his PhD here (1955). The Boston area is home to a vibrant academic environment formed by multiple universities with a strong tradition in programming languages and verification, and it is also home to several startups and tech industries related to these research areas. Thanks, Ankush
