Boston Computation Club (Max von Hippel)

Evan Boehs is a HIGH SCHOOL STUDENT who broke the freaking internet.  What more do I need to say?  Hire this kid.  Maybe I will.  It's a race.  

Evan made an npm package called everything which installs everything.  Then he got stuck in a dependency loop when someone tried to delete something.  It turns out this is a nearly impossible problem to solve and he totally broke npm.  Then a bunch of adults got made at him, when really, they should have been mad at themselves for building a bad system.  

You can read Evan's full story here: https://boehs.org/node/npm-everything

Bernardo Anibal Subercaseaux Roa
Marijn Heule. He has a background in engineering and is passionate about mathematics and computer science. Bernardo's research attacks the following question from a variety of angles: what can and cannot be done (efficiently?) by a computer? Today, Bernardo joined us to talk about Packing Chromatic, a fascinating research area at the intersection of pure mathematics and SAT solving. Bernardo and his advisor recently solved an open problem in the space, finding the packing chromatic number for the infinite 2D grid. We discussed the proof and a bunch of related problems, including some intriguing (and open) questions about periodic vs aperiodic tilings. By the way, this work was also covered (briefly) in the NYT! (Not a lot of 2nd year PhD students get covered in the grey lady!!)

Roger Waleffe is a PhD student in Computer Science at the University of Wisconsin-Madison working under the supervision of Prof. Theodoros (Theo) Rekatsinas (now at ETH Zurich). A few months ago one of our group members (Brennon) saw Rover's talk at EuroSys and thought it was pretty rad, so we invited Roger to give the same talk to the Club today. (You can decide, what's more prestigious, EuroSys or 6 random dudes from Boston?). Roger graciously agreed and gave a superb talk on MariusGNN, his recent work to make a blazingly fast, super resource efficient system for graph neural networks. We hope you enjoy the talk as much as we did!

Molly White is a Northeastern alum, a software engineer, and now, a web3 researcher (researching all the stuff that stinks about web3, to be clear).  Today Molly joined us to talk about her ongoing project and perhaps magnum opus, Web3 is Going Just Great (web3isgoingjustgreat.com), an ongoing history of all the grifts, thefts, hacks, and crashes in Web3/the broader blockchain ecosystem.  This was a fun one - perhaps even a controversial one - and we hope you enjoy it!

Nicholas Boucher is a PhD student in computer science studying under Professor Ross Anderson at the Cambridge Computer Laboratory.  He is also one of the authors of Trojan Source Attacks, a paper (and CVE, and vulnerability class) which highlighted supply-chain vulnerabilities in open-source software (among other things) due to code that is different than it looks.  This is one of the most creative hacks we saw in 2021 and we were thrilled to have Nicholas tell us about it.  The presentation was great, as was the discussion, where we got into the difficulties of the disclosure process, the complexities of peer review (in tandem with ethical vulnerability disclosure), and future problems (🤖🔔🐍🧶are emojis kosher??).  We hope you enjoy!

• Nicholas's homepage can be found HERE.
• You can read the Trojan Source Attacks paper HERE.
• You can see the video of this talk HERE.

Daniel Burgarth is an associate professor of mathematics at Macquarie University in Sydney, Australia, where he studies a host of interesting things including various kinds of quantum systems.  Today he joined us to discuss his 2014 Nature paper "Quantum Computing in Plato's Cave", which studied the complexity of quantum computers through a mathematically and philosophically structured lens.  This talk was a lot of fun, and the math was refreshingly easy to follow, despite the difficult topic.  The Q&A section was also quite good, although some of it was cut from the recording (hence why you should always come to events live!).  

• The paper 
• Daniel's homepage
• This presentation as a video

Todd Schmid
an Assistant Professor in the Computer Science Department of St. Mary's College of California. They are generally intereted in the algebraic, coalgebraic, and logical foundations of program semantics, and recently completed a PhD as a part of the PPLV group in the Computer Science Department of University College London. Today Todd joined us to talk about coequations, a fascinating (categorical) subject relating to the how we add algebraic structure to a space, how we think about relationships between spaces, and more. It turns out that coequations show up all over the place -- in DFAs, Markov chains, various PL concepts, etc. -- and so this is a place where the more abstract categorical stuff turns out to be really useful and illuminating for fairly concrete computer science ideas. Plus, coequations are just plain neat! We were really lucky to steal a little over an hour of Todd's time on this beautiful Saturday and we hope you enjoy the talk as much as we did.

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!

Joshua Ramette (https://x.com/RametteJoshua) recently completed a PhD in physics at Mass Tech, and today he joined us to talk about his new project, Undermind. Josh and his friend Tom Hartke (https://www.tomhartke.com/) founded Undermind (YC S24) to radically improve academic literature search using a mixture of AI techniques. Their system is slow, deliberate, and very high quality. You can check out Undermind at www.undermind.ai , or peruse the query I did during the Q&A section here: https://www.undermind.ai/query_app/display_one_search/c743b66ee4378b12ae8bad1fe58975ba95da71e7f7a1d5c2f0c6973c677648cc/

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.

John Viega is the Executive Vice President of Products, Strategy, & Engineering at SilverSky, an Adjunct Professor at NYU Poly, former editor-in-chief for IEEE Security and Privacy Magazine, co-developer of GCM (a mode of operation for block ciphers such as AES), and the original author of Mailman, the GNU Mailing List Manager.  He's also the founder of CrashOverride, a stealthy new security company which you should totally apply to work at!  Today he joined us to do an impromptu Q&A about his storied career as one of the people on the ground floor of cybersecurity, in its messy and exciting start.  This was a fun one and we hope you enjoy it as much as we did!

eta is a phenomenally talented polymath, hacker, and computer programmer from the UK.  Today eta joined us to discuss her very fun project reverse engineering UK rail tickets.  This was a fun event with a reasonably big audience and lots of Q&A, and we really enjoyed it!  It was also a good example of the best possible outcome in hacking: you break something, you tell the people who made the thing, and they give you a high-five and fix it.  Thank you so much eta for speaking to us!  To learn more about eta's work, refer to her website here: https://eta.st/

Today Nathaniel Mitchell and Dan Scott joined us from Intel to discuss the ChipSec project, an open-source platform security assessment framework, available at https://github.com/chipsec/chipsec .  Specifically, ChipSec "is a framework for analyzing the security of PC platforms including hardware, system firmware (BIOS/UEFI), and platform components" -- for both Windows and Linux (although as we discuss, getting it to work on Windows requires some leg-work).  This was a really interesting talk and it included a very impressive demo!  We learned a lot and we're very thankful that not just one but two busy engineers from Intel took the time to talk to us today about their fascinating software tool.

Max Ammann is a cybersecurity researcher at Trail of Bits, where he's recently been working on extending his Master's thesis work on fuzzing cryptographic protocols into an industrial-grade fuzzing tool. That work resulted in an S&P publication which is what he joined us to present today. This was a really good talk but also a great discussion, in large part because of the highly engaged audience (with representation from Galois, TwoSix, and academia!).

Navid Hashemi recently defended his PhD at USC and is about to begin a post-doc at Vanderbilt.  His research focuses on the intersection of Artificial Intelligence and Temporal Logics, with applications in Formal Verification of Learning Enabled Systems and Neurosymbolic Reinforcement Learning.  Today Navid joined us for a really exciting presentation about his work on metrizable logics for reinforcement learning, and a technique for verification thereof based on the over-approximation of reachable sets using ReLU.

Kai Bernardini is a professional hacker/security researcher, a mathematician, and and a lecturer in computer science at Boston University.  He's also better than me at lead belay (no short-roping from Kai!).  Today Kai joined us to discuss covert command and control (C2) channels.  Sure, your communication might be indistinguishable from random noise.  But is it indistinguishable from r/dankmemes?  If not, prepare to get caught by the local sysadmin. 

• Kai on Github
• Kai on Twitter
• This talk on YouTube

Evan Pu ( https://evanthebouncy.github.io/ , @evanthebouncy on X ) is a senior research scientist at Autodesk AI Lab, working on code-generation for human-machine collaboration in CAD, and industry scale instruction-following dataset annotation. Today Evan joined us from a toilet (with the lid closed) so as not to wake up his wife due to a rather large time-zone delta, which was hilarious and a first for the Boston Computation Club. Anyway, this was a really fun talk with excellent Q&A and we hope you enjoy it as much as we did!

Anthony Bonato is a Professor in the Department of Mathematics at Toronto Metropolitan University. Anthony's research focuses on graph theory, with applications to real-world complex networks and pursuit-evasion games on graphs such as Cops and Robbers. However, today Anthony joined us not to present some groovy new results in graph theory, but rather, to discuss how one _might_ give such a presentation, with panache! This was a super fun event with a lively and engaged discussion and we hope you enjoy it as much as we did.

- Anthony's webpage: https://math.ryerson.ca/~abonato/

- Anthony's Twitter: https://twitter.com/Anthony_Bonato

- This talk in video form: https://youtu.be/ZmLoQDWEZgg

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!

"Café Events" are small, informal events where we discuss our research and our (perhaps, unfulfilled) research interests.  Our ongoing "Biology Café" series is exactly that, but focused on topics at the intersection of biology and computation.  Today's presentation by Sophia von Hippel covered the open, and very important, problem of developing a mathematical language for chemistry.  Chemistry has a great diagrammatic syntax, but a (or, multiple) terrible prose representation.  Sophia presents the problem in clear and careful detail with examples, and then we discuss.  TL;DR: we don't solve the problem.  Sophia is currently pursuing a BS in Chemistry at the University of Arizona (with Honors).  She previously interned with NASA and served as a COVID-19 vaccinator.  She is also an Emergency Medical Technician with the University of Arizona Emergency Medical Services (UAEMS).  You can also view this presentation as a video on YouTube [HERE].

Joe Shiraef is a professional card counter and indie game dev.  Today he joined us for a very fun, free-form conversation on advantage play, indie game development, avoid arrest, and pursuing your passions.

https://www.inktalestudios.com/

Cory Doctorow (craphound.com) is a science fiction author, activist and journalist.  In my circles, he's probably best known for his work with the Electronic Frontier Foundation (EFF) and Boing Boing, but he's also a renowned science fiction author in his own right, an MIT Media Lab Research Affiliate, a Visiting Professor of Computer Science at Open University, a Visiting Professor of Practice at the University of North Carolina’s School of Library and Information Science, and co-founder of the UK Open Rights Group.  In short: Cory is precisely the kind of polymath we love to engage with at the Boston Computation Club!  Today, Cory joined us to discuss Big Tech - what's wrong with it and how to fix (read: DISMANTLE) it.  The talk was engaging, exciting, elucidating - all that and a bag of chips.  We really enjoyed talking to Cory and we hope you enjoy the recording!  You can also view this talk in video form HERE.

Eli Sennesh is a recent graduate of the PhD program in computer science at Northeastern, in which I (Max) and many other BCC group members are currently enrolled. Eli's research is highly interdisciplinary, taking into consideration various topics in mathematics (statistics, measure theory, probability theory, optimization), programming language theory, and neuroscience, with the unifying goal of building useful probabilistic programming languages. Today Eli joined us to discuss that research, with a particular emphasis on important open problems -- problems which he intends to study as a post-doc! This was a fun one and an excellent introduction to the world of probabilistic programming, and we really appreciate that Eli took time out of his weekend to come talk to us.

• Eli's website: https://esennesh.github.io/
• Eli's advisor's book on probabilistic programming: https://arxiv.org/abs/1809.10756

Maria is a PhD student in Computer Science at Purdue University, where she works with Dr. Dan Goldwasser on neural-symbolic methods to model natural language discourse, among other things.  Today she presented her recent project DRaiL, "an open-source declarative framework for specifying deep relational models, designed to support a variety of NLP scenarios."  

[ Paper ] [ Maria ][ Code ][ Video ][ Boston Computation Club ]

Ben Weintraub is a PhD student in computer science at Northeastern University, advised by Cristina Nita-Rotaru.  Today he joined us to present his paper *Structural Attacks on Local Routing in Payment Channel Networks*, which was accepted to the 2021 Euro S&P Blockchain workshop.  This is a fascinating paper studying a startlingly powerful attack strategy against payment channel networks.  We really enjoyed Ben's presentation and the subsequent discussion, which involved PhD students in computer science and economics, in addition to professional engineers and mathematicians.  You can learn more about Ben and his work here: https://ben-weintraub.com/

This talk is also available on YouTube HERE.

Today Brook Santangelo and John Sterrett

Today puzzle-maker Roger Barkan joined us to talk about the creation and solution of cave puzzles, a category of puzzle for which he's quite famous as a puzzle author. Jacob lead the conversation, using an interactive puzzle that he implemented with the help of ChatGPT (:0), and it was a ton of fun. We're super grateful to Roger for joining us today and we look forward to doing a follow-up event sometime in the future!

Jacob's interactive: https://bstn.cc/artifacts/jacobDenbeaux/cave.html

Buy Roger's book (you know you want to!): https://www.barnesandnoble.com/w/colossal-cave-collection-roger-barkan/1125542215

June Marcuse

Matteo Capucci is a PhD student at the University of Strathclyde in the MSP group, advised by Neil Ghani and Scott Cunningham.  He studies Applied Category Theory (aka ACT), specifically Categorical Cybernetics and Applied Topos Theory.  Today Matteo joined us to discuss the foundations of Categorical Cybernetics, in a wide-ranging conversation touching on lenses, feedback systems, dynamical systems, and more.  The conversation extended these ideas to distributed systems, model checking, cyber-physical systems, program sketching, and quantum systems, among other things.  This one was an absolute blast live and we hope you enjoy it after the fact in its audio form.  

You can read more about Matteo HERE. 

You can read more about the Boston Computation Club HERE.

You can watch this presentation in video form on YouTube HERE.

Artem is a PhD student in computer science at Northeastern University, advised by Professor Jan Vitek.  Prior to joining the Khoury PhD program, Artem worked as an Assistant Professor at Southern Federal University in Russia, where he earned his MSc and BSc.  Today Artem joined us to present about linear Haskell, a version of / feature-set for Haskell allowing "linear" types.  Artem explained linearity, why it might be useful, and why adding linear types to an existing (non-linear) language can be difficult - with Haskell as a case study.

• You can watch a video version of Artem's talk [HERE].
• You can learn more about Artem [HERE].

Plagiarizing Wikipedia: "Jean-Éric Pin is a French mathematician and theoretical computer scientist known for his contributions to the algebraic automata theory and semigroup theory."  He will also be our featured guest in a week, presenting The Generalized Star Height Problem.  In advance of his talk, he requested that the audience familiarize themselves with some basic mathematical definitions, such as "monoid" and "completion of a metric space".  To which end, I prepared a presentation, went through some light-weight peer review with random friends from the PL group at Northeastern, and then delivered this talk.  This is a fun little review on various useful topics in math, and also, a good refresher if you intend to attend Dr. Pin's talk.  I hope you enjoy!

Joel David Hamkins is a mathematician and logician at Oxford, where he studies the logic of the infinite. Today Joel joined us to talk about infinite dimensional games. As Joel explained, there are really three areas of mathematical inquiry related to games: Game Theory, as traditionally used in economics, ecology, etc.; the Theory of Games, which many CS students learn a little bit of in Complexity Theory; and the Logic of Games, which is really the camp where this talk falls. This was a totally intriguing talk in which pretty deep mathematical ideas naturally emerged from simple, playful premises. We really enjoyed it and we hope you do too! This talk is also available in video form, here.

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!

Jacob is a mathematician, computer scientist, and notably, co-organizer of the Boston Computation Club.  Today he joined us to give an interactive lesson on web-scraping, with Worlde-solving as a motivating case study.  This was a fun exercise and one we will almost certainly follow up on in the future.  We worked through parsing the ... DOM?  Is that the right word?  IDK.  And then entering text.  And then actually utilizing the feedback offered by the game to start interactively solving the puzzle.  We concluded with a brief conversation about the complexity of handling the clues in the context of words that have more than one of a given letter.

• CODE
• VIDEO

Avijit Ghosh is a Research Data Scientist at AdeptID and a Lecturer in the Khoury College of Computer Sciences at Northeastern University. He's a good friend of mine and was an element of my PhD cohort at Northeastern. He's also a well-respected researcher at the intersection of machine learning, ethics, and policy. You can read about some of his innovative and cross-disciplinary work, for example, in the New York Times.

David Widder is a Postdoctoral Fellow at the Digital Life Initiative at Cornell Tech, and earned his PhD from the School of Computer Science at Carnegie Mellon University. If you know me personally, you might remember David because he and I were simultaneously involved in parallel antics to fight non-consensual workplace sensors at CMU and NEU, respectively. Another funny coincidence is that David and I attended the same international boarding school program, called United World College. But most importantly -- David is a first-class researcher in the space of AI ethics.

Fabio Tollon is a South African philosopher of technology, currently completing a post-doc at the University of Edinburgh.  Coincidentally, he taught a philosophy of science class that my fiancé took as an undergrad! Fabio's research focuses on developing a robust meta-ethical grounding in our approach to the ethics of AI. Without rigorous conceptual apparatus, Fabio argues (and we concur) that we will be lost in our ethical analysis of these emergent and ubiquitous artificial systems.

TODAY, we hosted a wonderful panel discussion on AI ethics, with the above three panelists, and moderated by the long-time Boston Computation Club member, mathematician, and data-scientist Wei Sun. This was extremely informative, a lot of fun, and wildly interdisciplinary. Wei guided the discussion in a number of interesting discussions, and then the panelists fielded questions form the audience at the end. We didn't have enough time to answer everyone's questions but listeners are highly encouraged to email the panelists for follow-up :) .

I'd like to thank all the panelists and Wei again for showing up and making this event the special moment in time that it was, and the diverse and highly engaged audience for participating in this project. This was a lot of fun and highly intellectually stimulating, and I hope we can do more events like this in the future.

Annie Rauwerda is an internet personality and polymath with a background in neuroscience and data science.  She is also the host and operator of Depths of Wikipedia, a phenomenally popular meme page, Depths of Wikipedia, which you can read about HERE on Wikipedia.  Annie is also herself a frequent Wikipedia editor and author.  Today she joined us to talk about how Wikipedia can be charming, funny, and informative, all at once.  She showed us a variety of charming examples of Wikipedia in all its niche internet glory, and then answered a metric ton of questions about Wikipedia, the internet, Stack Exchange, etc.  This was a super fun event and one we really enjoyed.  We hope you enjoy it too!

Tyler Hobbs is a generative artist from Austin, Texas.  Bill Cresco is a geneticist who specializes in quantitative evolutionary genomics at the University of Oregon.  Today Tyler and Bill joined us for a wide-ranging discussion, seeded by the topic of "complexity".  The conversation was fascilitated by our two excellent moderators, Anya and Joe.  Anya studied studio art and environmental studies at Wellesley College and now works at Reed Hilderbrand, and Joe studied bioengineering at MIT and now works at Ginko Bioworks.  The conversation was wide-ranging and compelling, and we hope you enjoy it as much as we did!  

• Learn more about Tyler Hobbs HERE.
• Learn more about Bill Cresco and his lab HERE.
• Learn more about the Boston Computation Club HERE.
• Learn more about Anya HERE.
• Learn more about Joe: Just kidding, you can't, he is an internet ninja.
• Watch the video version of this talk HERE.

The SpiceDAO is a decentralized autonomous organization (DAO) which recently purchased a copy of the "Dune Bible", namely, the elusive and rare storyboard script for Alejandro Jodorowsky’s DUNE film.  As big Dune fans ourselves, and also as nerds interested in both the failures and opportunities of Web3, we were enormously excited to meet with a representative of SpiceDAO and discuss all things decentralized.  The discussion was lively, touching on sybil attacks, democracy, in-real-world legal and financial instruments, blockchain permanence, forking, and other issues!  We really enjoyed this open conversation and look forward to more events like it in the future.

• SpiceDAO website
• SpiceDAO twitter
• An article in The Verge about SpiceDAO
• Video version of this recording

Harry Eldridge is a Cryptography PhD student at Johns Hopkins, advised by Abhishek Jain and Matthew Green. His research (so far) touches on security and privacy implications of commodity hardware, which is a fascinating topic deserving of the mathematically disciplined, cryptographically informed approach his lab takes to such problems. Today Harry joined us to talk about his research into the problem of AirTag stalking, and how it can be ameliorated, while retaining acceptable performance, through cryptographic protocols. This was a very interesting talk with serious, real-world implications, and we hope you enjoy it as much as we did!

For this event, Holmes Wilson of Fight for the Future moderated a panel retrospective on the Pegasus malware. Our panelists were:

- Jonathan Rugman: Foreign Affairs Correspondent at Channel 4 News, BAFTA Award-winning journalist, visiting lecturer at University of London, and Senior Associate Fellow at RUSI.

- Raya Sharbain: education and communities coordinator at the Tor Project, and digital rights activist at the Jordan Open Source Association as well as the Digital Arabia Network.

- Elina Castillo Jimenéz: feminist human rights lawyer and digital activist at the Amnesty International Tech Lab.

- Prashant Anantharaman: former speaker at the club who completed his PhD at Dartmouth under Sergey Bratus and now works at Narf Industires. And …

- Hinako Sugiyama: international human rights lawyer and law professor at UC Irvine.

This was one of our best events ever and well worth the listen.

Matej Panciak holds a PhD in mathematics and is a software engineer at the Argument Computer Corporation, where among other things, he works on Lurk. Lurk is a LISP for defining computations that can prove (in the ZKP sense) that they ran, which is probably useful for all sorts of cool things we haven't thought of yet, but right now, is pretty important for doing stuff on-chain. (I can easily imagine this being applicable to building something like a dweb version of AWS ... in some theoretical future where FHE is so good that you can just trust randos to run code for you). Anyway, Matej presented a super rad intro to Lurk, gave us a code demo (it worked!) and then enjoyed our usual über-nerd conversational segment at the end.

Elizabeth Coppock is a linguistics professor at BU. He research focuses on foundational topics in truth, reference, quantification, and measurement in natural language semantics, through the lens of specific empirical puzzles. Recently, one of our group members (Cheng Zhang) expressed interest in Elizabeth's work as it might relate to his own research in programming languages, so we reached out to Elizabeth and asked if she'd be willing to present to the seminar group. (This is one of my favorite things about running the group: when a group member expresses interest in some research paper, we can simply invite the lead author to give a presentation!). Elizabeth graciously agreed and gave one of the best presentations we've had in months, full of fascinating real-world examples of the often surprising ways that we use "per" in the English language, and the underlying mathematical complexity of said usage. This was an enormously fun talk and we really hope you enjoy it as much as we did! And thank you again to Elizabeth for presenting!

Andrea Mambretti is a system security researcher at IBM Research Europe, Zurich Laboratory.  He received his Ph.D. from Northeastern University, in the SecLab under the supervision of Engin Kirda.  Since 2011, he's participated in several CTF competitions (Ictf, Ructf, Defcon and others) with both the TowerOfHanoi and Shellphish teams.  (Audience members will surely fall into two partitions: those who are more impressed by Andrea's PhD, and those who are more impressed by his membership in Shellphish 😉).  Today, Andrea joined us to discuss some of his security research into ROP attacks, specifically attacks that exploit timing-based side-channels caused by speculative execution.  This research builds on the academic legacy of attacks like Spectre, but formalizes the relevant threat models and explores the full space of relevant attack varieties.  The talk was fun, technical, and exciting.  We concluded with a question-and-answer/discussion section, mostly centered on (a) attack realizability against differing architectures, and (b) mitigations/defenses.  This was a great talk, and we hope you enjoy it post-hoc!

• ArXiV
• Andrea's homepage
• Andrea's twitter
• Video version of this talk

Today Christian Williams joined us to talk about his dissertation project, Logic in Color.  This is a really exciting project which he is now working on post-graduation, which aims to re-frame the way we think about logic, and logics, using a largely visual medium.  The key insight is that certain mathematical observations are made completely obvious simply by adding color to the areas enclosed by arrows in monoidal string diagrams.  But from this key observation comes the more foundational view that really, all of mathematics and logic not only can be expressed visually, but in some sense, perhaps _is_ visual; that the medium is exposing something fundamental about the nature of thought itself.  This sounds a little pretentious but it's actually just the opposite: it's a fairly radical effort to _simplify_ logic and category theory using a visual medium.  And it's enormously exciting.  We were really happy Christian gave us this ground-floor view on his project and we're super excited to see where it develops.

Today Richard Blythman joined us to talk about the big and exciting world of large language models. Richard has a PhD in fluid dynamics and is the CEO of Algovera, a cool company building a decentralized and personalized tech stack based on LLMs. His talk today was short and focused, explaining what in particular makes LLMs so magical. Then we had a phenomenal discussion section! We hope you enjoy it as much as we did. To learn more about Algovera, go here: algovera.ai

Derek Egolf is a PhD student (since 2021) at Northeastern University, advised by Stavros Tripakis. His primary research focus is the automatic generation of correct-by-construction systems from high-level specifications (synthesis). Today Derek talked about his recent paper in this vein, Efficient Synthesis of Symbolic Distributed Protocols by Sketching, to appear in FMCAD. This was a very interesting talk with a technical conversation afterword. We hope you enjoy it as much as we did!

Chengpeng Wang
working with Prof. Xiangyu Zhang. His research focuses on program analysis, especially software analysis, and in particular how existing analysis techniques intersect with emerging approaches from AI such as Large Language Models. Today Chengpeng joined us to talk about his recent NeurIPS paper proposing a novel static analysis technique based on LLMs. The technique is very interesting and highly informed by prior works in the static analysis space, but leverages LLMs as a kind of "oracle" to solve problems which, when handled statically, quickly become untenable. This was a really interesting talk and we're very greatful that Chengpeng took time out of his Sunday afternoon to talk to us!

Mathias Preiner is a Research Scientist at Stanford University in the Centaur lab. He is one of the main developers of the SMT solver Boolector (since June 2012) and Bitwuzla -- which is what he joined us to discuss today. This was a good talk, but an excellent Q&A, and we really enjoyed it. Thanks Mathias for joining us today, and to the awesome audience for showing up with such deep and technical questions!

Matt von Hippel is (a) my cousin and (b) a professor at the Niels Bohr International Academy in Copenhagen, Denmark, where he researches scattering amplitudes in gauge and gravity theories.  Matt received his PhD in 2014 from SUNY Stony Brook, and from 2014 to 2017 he was a postdoctoral fellow at the Perimeter Institute.  Today Matt joined us to discuss Feynman integrals.  Apparently "Feynman integral" means different things to different people; the kind discussed here are those associated with "Feynman diagrams".  The talk was engaging and fun, and at the end Matt fielded mathematical questions from the audience, which included both usual BCC members and some NEU mathematics faculty.  This was a fun one and I encourage you to watch it, if you didn't make the live event! 

• Matt's personal page at the NBIA is HERE.  
• Matt's popular physics blog is HERE. 
• Matt can be found on Twitter HERE.
• This talk can be found in video form HERE.
• You can learn more about the Boston Computation Club HERE.

Larkin Liu is an operations research (OR) & machine learning (ML) specialist, currently completing a PhD in Operations Research under the advisement of Stefan Minner at the Technical University of Munich.  Today Larkin joined us to present *An Extensible and Modular Design and Implementation of Monte Carlo Tree Search for the JVM*, a recent preprint he authored with Jun Tao Luo (MS student in CS at Carnegie Mellon; also in attendance at this talk).  The paper is exactly what it sounds like, and the presentation was a lot of fun, with clear mathematical background, a solid foundation in software engineering principles, and some impressive code demos.    

- Preprint: https://arxiv.org/abs/2108.10061 

- Larkin: https://larkz.github.io/ 

- Jun: https://www.linkedin.com/in/jun-tao-luo

- Video: https://youtu.be/bVpUlJU-piA

Shriram Krishnamurthi is a professor of Computer Science at Brown University, where he researches (among other things) programming languages, software engineering, formal methods, HCI, security, and networking.  Today Shriram joined us to discuss his joint project with Kathi Fisler, Benjamin S. Lerner, and Joe Gibbs Politz, titled "A Data-Centric Introduction to Computing".  The project is a new vision of what it means to teach introductory computing with data as a first-class object, in the form of tables.  This was a really excellent talk with a lively discussion touching on data quality, student motivation and engagement, pedagogy, data visualization, the nature of computation both essentially and in social context, incorrect assumptions programmers make (about names, interfaces, data, etc.), and much, much more.  We had a lot of fun with this one and we hope you enjoy it too!

By the way, you can watch the video version of this talk, HERE.

William Kretschmer is a PhD student at the University of Texas Austin, advised by Scott Aaronson.  He's one of these pseudo-celebrity-grad-students with lots of cool splashy results and we're stoked that he took the time to talk to us today.  The talk primarily covered the basics of quantum cryptography, much of which should be familiar to regular group members who attended our quantum cafe series with Billy, but also concluded with some groovy quantum crypto history (see: quantum cash) and a discussion of exciting recent results by William & co.  This is one of a series of cryptography related talks we're hosting this semester, and William started that series out with a bang!  We hope you enjoy!

Jan Hennecke is an engineer and roboticist in Boston, MA. Jan has been a buddy of mine for ages, ever since we met at the Bernardo Faria Jiu Jitsu Academy where he told me a hilarious story about placing top-3 in his first half ironman while munching down on snickers. Today Jan joined us to talk about his work at RBTX, a marketplace and platform for low-cost automation. This was a really fun talk with a lot of audience engagement and I think many of you will find it interesting!

Carlo is a postdoc in the Computer Science Department at Carnegie Mellon University, where he received a Ph.D. under Robert Harper. He previously studied at Indiana University Bloomington, where he received a B.S. in Mathematics and in Computer Science.  Today Carlo joined us to discuss Homotopy Type Theory, a new foundations for mathematics based on a recently-discovered connection between Homotopy Theory and Type Theory.  Carlo explains intuitively what Homotopy Type Theory is and how it is used, and then goes over various possible implementations of Homotopy Type Theory in a theorem-proving environment such as Coq.  Finally, he fields questions on Homotopy Type Theory, theorem-proving, and other topics from the Boston Computation Club audience.

• The Boston Computation Club can be found at https://bstn.cc/
• Carlo Angiuli can be found at https://www.cs.cmu.edu/~cangiuli/
• A video recording of this talk is available at https://youtu.be/VMqF06fDljU
• For more on Homotopy Type Theory refer to https://homotopytypetheory.org/book/

Adam Karvonen was my coworker at Galois and is a bright guy doing really interesting stuff in the ML interpretability space. Today he joined us to present his work on Chess-GPT, you guessed it, a GPT model that can play chess. The punchline isn't so much how good the model is as it is how the model "thinks" -- Adam provides compelling evidence that the model internally reasons about an actual board state, and learns to make legal moves. The discussion on this one was great and we really appreciate that Adam took the time to talk to us! Also -- you should hire him! He's doing MATS but will be on the job market at the end of the Summer.

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!

Ian Bicking is an engineer at Brilliant, which is also what he is. (Sorry, dad joke). Ian joined us today to talk about his super charming (and extremely interesting) weekend of experiments hacking various LLMs to solve puzzles using z3. The presentation was roughly the first 2/3 of the event and the remaining third presented a fantastic conversation about the future of AI, tool use, chain and tree of thought, o1, and more. Thanks again for joining us Ian!

Arthur O’Dwyer is a C++ programmer and blogger who today joined us to talk about his musings on the algebraic structure of the popular web-game Infinite Craft. Infinite Craft is a clever little experiment in sandboxed exploration, and it turns out to give rise to a rather complex mathematical structure with some interesting background in theoretical CS. Arthur covered all this and more in his presentation, which was super interesting and a lot of fun to watch.

Check out Arthur's original blog post here: https://quuxplusone.github.io/blog/2024/03/03/infinite-craft-theory/

Check out Arthur's slides here: https://bstn.cc/artifacts/arthurODwyer/infiniteCraft.pdf

John Ryter is my lead partner in Cambridge MA, a gnarly climber, and also a PhD student in materials science at MIT (aka MassTech) where he studies recycling using a unique combination of economic theory and environmental modeling.  John's work has entertained me during countless climbing sessions and now it can equally enthrall you, via the magic of the Internet.  We were very happy to have John present to the group, particularly since the audience contained a chemist, a physicist, and a geo-physicist, in addition to the standard array of derelict computer scientists (myself included).  To read more about John's work, refer here.  You can also watch this talk on YouTube, here.

Matthias is a world-class scientist and highly influential computer programmer, and also the author of "How to Design Programs", a Computer Science 101 book which takes a fundamentally different approach than prior works. Today Matthias joined us to share his experience writing that book (and its many iterations), as well as his broader philosophy on how to instruct the next generation of thinkers and builders (not to mention, programmers). This was a highly instructive and somewhat philosophical talk and we really hope you enjoy it as much as we did! To learn more about Matthias, refer here: https://felleisen.org/matthias/

LakYah Tyner is a 1st year PhD student at Northeastern University co-advised by abhi Shelat and Daniel Wichs.  Her research focuses on cryptography, with recent works involving Property Preserving Hashing and Threshold Signature Schemes.  Put differently, she's accomplished considerably more in less than a year of graduate school than I did as a first year (we're a semester in and she has a paper in Crypto!), and today she joined the Boston Computation Club to share some of that hard-earned wisdom.  LakYah's talk focused on the difficult problem of efficiently hashing data such that the hashes preserve a binary predicate relationship from the pre-image, specifically a relationship relating to the distance between the two compared objects.  This is a fascinating topic with implications for systems like Apple's facial recognition and attempts at privacy-preserving CSAM detection.  We're super stoked LakYah agreed to speak to us today and we hope you enjoy her talk as much as we did! 

• LakYah's website: https://www.khoury.northeastern.edu/home/lakyahtyner/index.html 
• The paper: https://eprint.iacr.org/2022/842

Dhekra Mahmoud
at LIMOS in Clermont-Ferrand, France, where she researches the formal analysis of cryptographic protocols under the supervision of Pascal Lafoucade and Jannik Dreier. Today Dhekra joined us to present her recent USENIX paper Shaken, not Stirred -- Automated Discovery of Subtle Attacks on Protocols using Mix-Nets. This was a really interesting presentation with a good conversation afterword touching on some subtler points around the Dolev-Yao threat model, the limitations of ProVerif, and proof optimization.

Roughly four years ago, when I took second semester Abstract Algebra at the University of Arizona, my professor (Jay Taylor) generously offered to meet with me every week outside class to discuss algebraic topics in computer science.  We chose Dr. Pin's book, Varieties of Formal Languages.  Due to my own mathematical immaturity we worked through the material slowly, and didn't finish the text before I graduated.  Nevertheless, working through this material helped inspire me to pursue a PhD in formal methods - an endeavor I'm solidly halfway through at the time of writing.  All this is to say, Jean-Eric Pin is partially to blame for the fact that I am currently a sleepless PhD student at Northeastern University.  

Today Jean-Eric Pin joined us to discuss The Generalized Star Height Problem, an open problem in formal language theory which he and his colleagues have attempted to attack from all angles: algebraically, logically, topologically, etc.  It's one of those deeply enticing problems in math that's reasonably easy to explain yet apparently quite challenging to solve.  In this 2-hour talk, Jean-Eric Pin explains the problem starting with the most basic definitions, and then discusses some of the related results from those who wish to solve it.  It's a fascinating and very accessible talk, and we really hope you enjoy!

You can view a video version of the talk HERE.

Sara Archour recently completed a PhD at MIT/CSAIL in Computer Science and Artificial Intelligence, and is joining Stanford University (EE) as an Associate Professor. Sara studies analog computers - how to build them; how to use them; what they're good for; how to stick them together to do interesting things; and so forth. Today, Sara joined us to discuss these things, with a smidgeon of career advice at the end :)

• Sara Archour's homepage can be found HERE.
• This presentation can also be viewed in video format HERE.

Ankit Kumar is a PhD student in the Khoury College of Computer Science at Northeastern University, advised by Pete Manolios.  He is from Dhanbad, Jharkand, in India, and prior to joining Northeastern, he earned his MTech in Computer Science and Engineering from IIT Kanpur and his BTech in Electrical Engineering from IIT (BHU) Varanasi.  Now, Ankit's research focuses on formal methods (FM) -- particularly in ACL2Sedan -- and the use of FM to study programming languages, including writing machine-checkable proofs to prove properties.  Today Ankit joined us to present Mathematical Programming Modulo Strings, his recent FMCAD21 paper.  This presentation can be viewed as an "extended" version of the 10-minute presentation he gave at that conference.  

- Ankit Kumar: https://www.khoury.northeastern.edu/people/ankit-kumar/

- FMCAD21: https://fmcad.org/FMCAD21/

- Pete Manolios: https://www.ccs.neu.edu/~pete/

- The Boston Computation Club: https://bstn.cc/

- Video form of this talk: https://youtu.be/doeauZv3JrE

Bo Zhao is a 2nd year PhD student in computer science at UCSD, advised by Rose Yu. Her research focuses on deep learning theory and optimization, with a recent emphasis on the parameter space and dynamics of learning. Today Bo joined us to talk about her recent paper, "Symmetries, Flat Minima, and the Conserved Quantities of Gradient Flow", which was joint work at ICLR with Iordan Ganev, as well as co-authors Robin Walters, Rose Yu, and Nima Dehmamy. This is a really interesting paper which takes an algebraic approach to a problem typically only studied analytically. Bo gave a phenomenal presentation and then we had a really nice discussion with a variety of technical questions. We enjoyed this one a lot and we hope you do too!

Kimberly Ayers is an assistant professor of mathematics at Cal State San Marcos, where she studies the mathematics of hybrid systems.  Kimberly is a genuine theorist (in contrast to us computer science neanderthals, haha) and this talk touched on some of the aspects of hybrid systems that make them theoretically interesting (e.g.,  how the topology imposed on a skew flow can apparently be quite strange).  Since I've only previously seen hybrid systems work in CS, where it's always motivated by practical justifications like "Boeing", this was refreshing and cool!  Anyway we had a really nice time with a great conversation section, and if you missed it, I'm sure you'll thoroughly enjoy the recording.  You can read more about Kimberly HERE.

Bill Dalessandro is a philosopher of science and mathematics at Oxford University. Today Bill joined us to discuss proofs -- specifically, what it means for a proof to be fixable, what it means for a proof to be transferable, and the apparent tension between these notions. This work built on prior work by Northeastern's Don Fallis, who attended the talk and participated in the lively and fascinating conversation that ensued. We also discussed what it's like to work in an interactive theorem prover. In such an environment, you don't really make mistakes -- because the prover doesn't let you -- but you might prove the wrong thing, and/or, you might not learn much despite having proven something. This was a great talk with a great with a really strong discussion section and we hope you enjoy it as much as we did! - Bill's website - The paper in question

Mel Andrews is an instructor and doctoral student in the department of philosophy at the University of Cincinnati.  Their work focuses on the phenomena of cognition and life, comparing and contrasting the merits and explanatory scope of conceptual and formal models of life and mind, and exploring the implications of these considerations for science at large.  Today Mel joined us to talk about the philosophy of math in science and mathematical models in scientific reasoning.  How do models relate to the real world?  When can models tell us something about ... anything other than their own mathematical substance?  And perhaps most importantly, in the Q&A section, how can we build a formal mathematics for computer hacking 😉?  This was a super fun event and we are very thankful for Mel's time.  We hope you enjoy it as much as we did!

Christopher Ba Thi Nguyen is a professor of philosophy at the University of Utah, and the author of Games: Agency as Art. Today he joined us to discuss his book, which covers the philosophy of all sorts of games: rock climbing, Dark Souls, judo, poker, dungeons and dragons, etc. The event took the form of an interview hosted by Wei Sun, a longtime group member who read Thi's book in detail and really vibed with it. This was one of the most engaged and dynamic conversations we've hosted and in contrast to other events which have had a heavily visual component, this one is mostly auditory, so should make a very good podcast-style experience. We're very grateful to Thi for joining us today and to Wei for hosting the event, and we hope you enjoy it post-hoc as much as we did live!

- The book: https://www.amazon.com/Games-Agency-As-Art-Thinking/dp/0190052082- Wei's blog: http://weiright.blogspot.com/2022/06/movie-review-everything-everywhere-all.html

- Wei's blog: http://weiright.blogspot.com/2022/06/movie-review-everything-everywhere-all.html

Julia Belyakova is a PhD student in computer science at Northeastern University, where she is currently focused on formalizing the Julia programming language.  Julia's primary primary research interests are programming languages and type theory, although she also enjoys theorem proving, generic programming, functional and object-oriented programming, software engineering, programming by contracts, software testing, and as of late, human aspects of software engineering and the interaction between humans and programming languages.  In short: Julia is quite the polymath.  Today she joined us to discuss the Julia Language's type system, in contrast to type systems in other languages, and in programming language research papers.  This was a really fun talk and also a very accessible entry-point to the topic for those without a strong PL background.  We hope you enjoy!  

- Julia Belyakova's homepage: https://julbinb.github.io/

- The Julia language: https://julialang.org/

- The Boston Computation Club: https://bstn.cc/

- This talk but as a video: https://youtu.be/JNxrX2XvZIY