[Eecs_msee] ChBE seminar: Monday, Sept 30: Dr. Tyler Josephson

[Hunter, Tiffany]

 Dear all,



Our seminar speaker for Monday is Dr. Tyler Josephson, Assistant Professor of Chemical, Biochemical, and Environmental Engineering at the University of Maryland, Baltimore County. The title of his talk is "Writing Provably-Correct Software using Lean". I met him this summer during a conference and learned that he is using a software language to write and check mathematical derivations, which I found to be quite exciting. Below are the details of his seminar:



Writing Provably-Correct Software using Lean



When developing new methods for molecular simulation, eliminating bugs can be challenging. Programming languages like Python, FORTRAN, and Julia flag syntax errors, but don't (and cannot) catch errors in math or program logic - these must be rooted out by human experts. These issues can be managed by following best practices in software development (such as writing tests alongside the program), but even these do not guarantee that code is correct. Probabilistic programs like Monte Carlo are especially notorious.

Lean is a new programming language whose type system enables it to describe and check the logic of advanced math proofs. By translating derivations in science and engineering into math proofs in Lean, we get a computer-checked proof that the derivations are mathematically and logically correct. We've translated the derivations of Langmuir and BET adsorption theory, as well as proofs about ideal gas thermodynamics and the kinematic equations of motion [1]. We can also write software for scientific computing in Lean, and write proofs about the functions in our execution pipeline, providing guarantees that they have certain properties. Our prototype program performs BET surface area analysis using functions that are logically connected to a formal derivation of BET adsorption theory. In the future, we aim to build LeanMD and LeanMC, formally-verified molecular dynamics and Monte Carlo software logically linked to formal derivations in classical and statistical mechanics.

[1] Bobbin, M., Sharlin, S., Feyzishendi, P., Dang, A. H., Wraback, C. M., Josephson, T. R., ``Formalizing chemical physics using the Lean theorem prover." Digital Discovery, (2024)

https://doi.org/10.1039/D3DD00077J<https://nam11.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdoi.org%2F10.1039%2FD3DD00077J&data=05%7C02%7Ceecs_msee%40listserv.ohio.edu%7C07a55689f9064815512808dcdda4ab50%7Cf3308007477c4a70888934611817c55a%7C0%7C0%7C638628946551141914%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=hJZHia5k5DDb%2BXJrGpgrKMor%2BpzNmm3EZFawhV9H%2FLk%3D&reserved=0>



This work is primarily supported by the NSF CAREER Award #2236769







[A person wearing glasses and a suit  Description automatically generated]Dr. Tyler R. Josephson is an Assistant Professor in Chemical, Biochemical, and Environmental Engineering at the University of Maryland, Baltimore County. He received his B.S. in Chemical Engineering from the University of Minnesota in 2011 and his Ph.D. in Chemical Engineering from the University of Delaware in 2017, after which he was a postdoctoral associate in the University of Minnesota Chemistry Department until 2020. In 2018, he spent time as a visiting scientist in the Mathematics of AI department at IBM Research. At UMBC, he leads the AI & Theory-Oriented Molecular Science (ATOMS) Lab, developing computational methods for molecular simulation and automated discovery of scientific theories. Techniques used in the ATOMS Lab include quantum chemistry, Monte Carlo, symbolic regression, and formal theorem proving using Lean. Dr. Josephson received the NSF Graduate Research Fellowship and is the 35th Laird Fellow at the University of Delaware. His research is supported by the National Science Foundation and the Department of Energy, including the NSF CAREER Award for "Automated Reasoning to Advance Chemical Theory."





Sumit Sharma
Associate Professor

Department of Chemical and Biomolecular Engineering

181 Stocker Center
1 Ohio University
Athens OH 45701-2979
T: 740.593.1425

M: 503.209.7165

sharmas at ohio.edu<mailto:sharmas at ohio.edu>

website: http://sharma-research.com/<https://nam11.safelinks.protection.outlook.com/?url=http%3A%2F%2Fsharma-research.com%2F&data=05%7C02%7Ceecs_msee%40listserv.ohio.edu%7C07a55689f9064815512808dcdda4ab50%7Cf3308007477c4a70888934611817c55a%7C0%7C0%7C638628946551141914%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=8uOEsNT4X9DKIut82J6ZD8fjH7Pz2eEI4cgh%2B95A69k%3D&reserved=0>

[cid:image006.gif at 01DB0F48.99040100]

Russ College of Engineering and Technology


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://listserv.ohio.edu/pipermail/eecs_msee/attachments/20240925/475a889d/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image006.gif
Type: image/gif
Size: 2968 bytes
Desc: image006.gif
URL: <http://listserv.ohio.edu/pipermail/eecs_msee/attachments/20240925/475a889d/attachment.gif>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image001.jpg
Type: image/jpeg
Size: 7607 bytes
Desc: image001.jpg
URL: <http://listserv.ohio.edu/pipermail/eecs_msee/attachments/20240925/475a889d/attachment.jpg>