Boston Computation Club

Max von Hippel

The Boston Computation Club is a small seminar group focused on mathematical computer science, and computational mathematics. Its name is plagiarized from the London Computation Club. Boston Computation Club meetings occur roughly every other week, on weekends, around 5pm EDT (modulo speaker availability). The usual format is a 20m presentation followed by 40m of discussion. Some, but not all, meetings are posted on YouTube and in podcast form.

Listen in PodNod RSS feed Show website

20 episodes
Updated July 3

Episodes20

Newest first

July 3 · 48 min
06/26/26: Tracing Introspection Across Model Depth, Zach Maas
Zach Maas is an independent AI safety & mechanistic interpretability researcher in Boulder, Colorado, funded by Coefficient Giving. Today Zach joined us to talk about some of his recent work tracing introspection across model depth. This is, I think, the first mech interp talk we've hosted other than ChessGPT, and it was a good one! We hope you enjoy it as much as we did!
April 18 · 58 min
An Extremely Short Proof of the Hairy Ball Theorem with Peter McGrath
Today Peter McGrath An Extremely Short Proof of the Hairy Ball Theorem. Peter is a professor of mathematics at NC State, where he researches geometric analysis, minimal surfaces, PDEs. Today's talk was an elegant presentation of the classical result -- Peter makes it accessible, and explains each concept in a clear and transparent manner. This was a really fun talk and really back to our roots as a group, doing pure math on an iPad and loving it! We hope you enjoy the talk as much as we did!
March 9 · 57 min
Logic.py: Bridging the Gap between LLMs and Constraint Solvers with Pascal Kesseli
Pascal Kesseli is a software engineer and technical lead at Microsoft AI, with a PhD in Computer Science from Oxford (or a DPhil? Or whatever they call PhDs on that side of the pond). Today Pascal joined us to discuss work he completed while at META FAIR, focused on the conjoining of large language models with symbolic reasoning systems (ultimately, dispatch to SAT) as well as future research directions building on said work.
February 18 · 48 min
2/17/26: Approximately Aligned Decoding with Daniel Melcer
Daniel Melcer is a PhD student at Northeastern University, where he researches formal methods, reinforcement learning, and large language models, among other things. Daniel also has the most colorful hair in the business (bright red for this talk, other colors for other occasions). Today he joined us to talk about some really exciting work he completed at Amazon, and to expand on his general vision of where constrained inference problems are heading in the future.
February 7 · 54 min
02/06/26: Early experiments in FMxAI at Galois with Max von Hippel
Max von Hippel is ... me, the organizer and founder of the Boston Computation Club. Today I hosted an extremely informal event to chat about some of the early experiments in FMxAI I was involved with at Galois, two years ago.
January 17 · 41 min
VeriExploit: Automatic Bug Reproduction in Smart Contracts via LLMs and Formal Methods, Chenfeng Wei
Chenfeng Wei is a PhD student at the University of Manchester, where he researches formal guarantees for large language models. Today he joined us to talk about his latest work exploring bugs in smart-contracts. This is a really interesting project at the intersection of explainable AI, smart contract debugging/security, and cybersecurity/symbolic analysis, and I hope you enjoy it as much as we did!
January 5 · 57 min
Breaking the Sorting Barrier for Directed Single-Source Shortest Paths - Xiao Mao
Today Xiao Mao joined us to discuss his groundbreaking work, Breaking the Sorting Barrier for Directed Single-Source Shortest Paths. It's not every day you beat Djikstra at something. This was a good one. Thank you for talking to us, Xiao!
Sep 15, 2025 · 59 min
Infecting Generative AI with Viruses - David A. Noever and Forrest McKee
David A. Noever and Forrest McKee are researchers at PeopleTec, where they work on problems at the intersection of security, defense, and AI/ML. Today David joined us to present their joint work Infecting Generative AI with Viruses. This was a really great presentation that took a rigorous approach to defining the security boundaries and limitations of AI tools, and it fostered one of the better discussions we've hosted in a while. We hope you enjoy it as much as we did!
Aug 15, 2025 · 57 min
08/15/25: An LLM Agent for Functional Bug Detection in Network Protocols with Mingwei Zheng
Mingwei Zheng a Ph.D. candidate in the Department of Computer Science at Purdue University, advised by Prof. Xiangyu Zhang since 2021. Before that, she received her Bachelor’s degree in Computer Science and Technology from Huazhong University of Science and Technology in 2020. Mingwei's research lies at the intersection of Large Language Models (LLMs) and Software Engineering. She builds LLM agents that combine program analysis with LLMs for deep codebase understanding that improve software correctness, robustness, and trustworthiness. Today Mingwei joined us to discuss some ongoing work which she previously presented at IEEE Security and Privacy LangSec, applying language models to bug detection in protocols with IETF RFCs. This was a great talk with deep, technical content and a good conversation. We hope you enjoy!
Aug 2, 2025 · 1 hr 13 min
08/01/25: Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification with Kaiyu Yang
Today Kaiyu Yang from Meta joined us to discuss formal reasoning using LLMs, particularly in the context of interactive theorem provers. This is a really fast-moving and exciting field in which reinforcement learning and theorem proving combine to provide a new frontier for fully automated reasoning, and Kaiyu is at the bleeding edge of it. We were really lucky to get an hour of Kaiyu's time and we hope you enjoy the talk as much as we did!
Jul 25, 2025 · 52 min
07/25/25: RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types with Michael Sammler
Michael Sammler n assistant professor leading the Programming Languages and Verification Group at the Institute of Science and Technology Austria (ISTA). Today he joined us to talk about his three primary projects: RefinedC, which uses a refinement and ownership type system to verify C code, Islaris, which shows how to scale verification of assembly code to realistic models of real-world architectures, and DimSum, which provides a decentralized approach for reasoning about multi-language programs (with a particular focus on RefinedC). We had a small but really dedicated crowd which facilitated an excellent discussion. This was a really fun one and we hope you enjoy it as much as we did!
Jun 22, 2025 · 1 hr 41 min
06/20/25: TypeScript Types Can Run DOOM with Dimitri Mitropoulos
Dimitri Mitropoulos is a Michigan-based typescript dev, linguist, and classicist who joined us to talk about his completely unhinged, odyssean, and frankly just unwise project to get DOOM running completely within Typescript's type system. Someone give the dude a PhD, please.
Jun 14, 2025 · 59 min
06/13/25: Gradual Verification with Jenna DiVincenzo
Jenna DiVincenzo is an Assistant Professor in the Elmore Family School of Electrical and Computer Engineering @ Purdue University. She is broadly interested in research spanning software verification, programming languages, and software engineering, especially research aimed at making verification techniques and programming languages more usable and scalable. Today Jenna joined us to talk about her broad research program in gradual verification. This was a really interesting talk with great Q&A and we hope you enjoy it as much as we did!
May 8, 2025 · 39 min
05/07/25: Exploring Zero-Shot Prompting for Generating Data Format Descriptions, Prashant Anantharaman
Prashant Anantharaman is a long-time BCC group member and has presented as both a solo researcher and a panelist to prior events. Today he joined us to present some of his work with NARF, to appear at IEEE S&P, on generating grammars for fuzzing using LLMs. This is a super exciting new frontier for LLMs and LangSec generally and his talk was wonderful.
Apr 19, 2025 · 1 hr
04/18/25: Descriptive Complexity with Ramit Das
Ramit Das is a formal verification engineer at Intel and an avid Boston Computation Club group member. Ramit and I have been speaking for ages about formal methods, exchanging papers, etc. and today he finally agreed to come give a talk to the group about his area of expertise -- descriptive complexity. This was a really fun talk and an excellent introduction for anyone looking to get their feet wet with complexity theory, some language theory, and even a smidgeon of model theory and underpinnings of abstract interpretation. It was really fun and we can't wait to host another talk by Ramit sometime in the future!
Apr 5, 2025 · 52 min
03/21/24: How and Why to extend First Order Logic for Knowledge-Based Systems with Marc Denecker
Today Marc Denecker joined us to present How and Why to extend First Order Logic for Knowledge-Based Systems. This presentation provided the setup for a follow-on that Marc's student Simon Vandevelde is set to give on IDP-Z3, a formal reasoning machine that Marc and Simon have built. This was a really interesting talk touching on a variety of forms for formal logic, decision procedures, and industrial use-cases thereof, potentially with profound implications for the future and realizability of so-called AGI.
Apr 5, 2025 · 58 min
04/04/25: Constrained Decoding for Code Language Models via Efficient Left and Right Quotienting of Context-Sensitive Grammars with Daniel Melcer
Today Daniel Melcer joined us to present Constrained Decoding for Code Language Models via Efficient Left and Right Quotienting of Context-Sensitive Grammars (https://arxiv.org/pdf/2402.17988). This is work he completed while at Amazon, and it's a really interesting project around how to constrain, guide, and check language models such that they generate valid code within a given context. We really appreciate that Daniel took the time to talk to us and hope you like the talk as much as we did!
Mar 8, 2025 · 1 hr 2 min
03/08/25: An Introduction to LiquidHaskell with Michael H. Borkowski
Michael H. Borkowski is an Assistant Professor of Practice in the Department of Computer Science at Purdue University. Before joining Purdue, he earned his Ph.D. from the Department of Computer Science and Engineering at UC San Diego, where he was affiliated with the ProgSys Group. Today Michael joined us to discuss LiquidHaskell, a very cool project that incorporates a kind of refinement types, with SMT-based proofs, into Haskell. This was a really compelling talk and we hope you enjoy it as much as we did!
Jan 10, 2025 · 58 min
01/10/25: Combining Causal Inference and Knowledge Graphs with Brook Santangelo and John Sterrett
Today Brook Santangelo and John Sterrett
Jan 10, 2025 · 1 hr
01/04/25: Hacking GenAI with LLM Red Teaming and Beyond with Gaspard Baye
Gaspard Baye is a Cyber AI Ph.D. Candidate at the University of Massachusetts Dartmouth, where he researches AI-driven offensive and defensive security applications. Today Gaspard joined us to present "Hacking GenAI with LLM Red Teaming and Beyond" based on his recent DefCon talk. This was a really fun event with a great Q&A. Thanks to Jacob from the Trust Lab for hosting!

Boston Computation Club

06/26/26: Tracing Introspection Across Model Depth, Zach Maas

An Extremely Short Proof of the Hairy Ball Theorem with Peter McGrath

Logic.py: Bridging the Gap between LLMs and Constraint Solvers with Pascal Kesseli

2/17/26: Approximately Aligned Decoding with Daniel Melcer

02/06/26: Early experiments in FMxAI at Galois with Max von Hippel

VeriExploit: Automatic Bug Reproduction in Smart Contracts via LLMs and Formal Methods, Chenfeng Wei

Breaking the Sorting Barrier for Directed Single-Source Shortest Paths - Xiao Mao

Infecting Generative AI with Viruses - David A. Noever and Forrest McKee

08/15/25: An LLM Agent for Functional Bug Detection in Network Protocols with Mingwei Zheng

08/01/25: Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification with Kaiyu Yang

07/25/25: RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types with Michael Sammler

06/20/25: TypeScript Types Can Run DOOM with Dimitri Mitropoulos

06/13/25: Gradual Verification with Jenna DiVincenzo

05/07/25: Exploring Zero-Shot Prompting for Generating Data Format Descriptions, Prashant Anantharaman

04/18/25: Descriptive Complexity with Ramit Das

03/21/24: How and Why to extend First Order Logic for Knowledge-Based Systems with Marc Denecker

04/04/25: Constrained Decoding for Code Language Models via Efficient Left and Right Quotienting of Context-Sensitive Grammars with Daniel Melcer

03/08/25: An Introduction to LiquidHaskell with Michael H. Borkowski

01/10/25: Combining Causal Inference and Knowledge Graphs with Brook Santangelo and John Sterrett

01/04/25: Hacking GenAI with LLM Red Teaming and Beyond with Gaspard Baye