This is my (Henry Blanchette’s) website. The purpose of this website is to informally share my projects and items of interest for public reference. Some common topics are computics, software engineering, mathematics, philosophy, game theory, game design, politics, and (crypto)economics.
Profiles
Research
My research interests have centered around programming languages, simulation, mathematical modeling, and data analysis.
| time | topic | association |
|---|---|---|
| 2022-2023 | Liquid Flex – extension of the Flex language with refinement types | with Tangram |
| 2022-2023 | Pantograph – a zipper-interfaced well-typed structural editor | with Jacob Prinz; at University of Maryland |
| 2022 | Zypr – a zipper-interfaced structure editor | with Jacob Prinz; at University of Maryland |
| 2022 | Shape – a well-typed structure editor | with Jacob Prinz; at University of Maryland |
| 2022 | Liquid Proof Macros (acm) – tactical metaprogramming for Liquid Haskell proofs | with Leonidas Lampropoulos and Niki Vazou; at University of Maryland |
| 2021 | Block Types – generating dependently-typed terms using type-preserving mutations | with Jacob Prinz; at University of Maryland |
| 2021 | Extensional Equality in Liquid Haskell | with Leo Lampropolous, Niki Vazou, and Michael Greenberg; at University of Maryland |
| 2020 | Generalized Price Equation | with Mark Bedau; for the Artificial Life Lab at Reed College |
| 2020 | Separation Logic in Agda | with Jim Fix; at Reed College |
| 2019 | Gradual Verification | with Jonathan Aldrich; for REUSE at CMU |
| 2018 | Reputation in Academic Citation Networks | with Eitan Frachtenburg; at Reed College |
| 2018 | Vector Calculus Vizualizations | with Kyle Ormsby for Project Project; at Reed College |
| 2017 | Milnor Fibration Vizualizations | with Kyle Ormsby; for Project Project at Reed College |
Education and Employment
My education has centered around mathematics, computer science, and philosophy. My employment has been in software engineering, theoretical computer science research, and software verification.
| time | event |
|---|---|
| 2022-2023 | worked as independent contractor at Galois with Tangram |
| 2022 | worked as summer intern at Galois, developing the Cryptol langauge and verifying cyber-physical systems using Coq |
| 2021 | worked as summer intern at Runtime Verification, verifying Ethereum smart contracts using the K Framework |
| 2020 | began PhD program in computer science at University of Maryland |
| 2020 | graduated undergraduate program at Reed College with BA in computer science. Thesis: Purity and Effect |
| 2016 | began undergraduate program at Reed College |