<div dir="auto"><div dir="auto">Dear 手足s ("fellow (human rights/dissident) advocates" in Cantonese, originated in Hong Kong people's protests against China) in the movements of open source (and open science),</div><div dir="auto"><br></div><div dir="auto">Here are the keywords I mentioned today with the microtalk about formal methods in software:</div><div dir="auto">- formal methods, software analysis, formal verification</div><div dir="auto">- lambda calculus, type theory, calculus of inductive constructions, Church encoding, Turing completeness, strong normalization, soundness</div><div dir="auto">- TypeScript, PureScript, Haskell, generalized algebraic data type, inductive data type</div><div dir="auto">- structural induction, higher induction</div><div dir="auto">- Gödel's second incompleteness theorem, diagonal argument, Lawvere's fixed-point theorem</div><div dir="auto">- mutability, immutability, borrow checker (rust)</div><div dir="auto">- Hoare logic, separation logic</div><div dir="auto">- Coq, Lean, Agda, Idris</div><div dir="auto">- Verified C, Rustbelt, DeepSpec</div><div dir="auto">- Satisfiability Modulo Theories, Solidity (ethereum) SMT</div><div dir="auto">- Verified LLVM, Coq extraction</div><div dir="auto">- BC Pierce UPenn, Thierry Coquand UGothenburg, Adam Chlipala MIT</div><div dir="auto"><br></div><div dir="auto">Hope y'all join the revolution! Ask me anything if you're interested in formal methods, theoretical computer science, mathematics, or just anything. Ask me to come hangout too!</div><div dir="auto"><br></div><div dir="auto">Pride and solidarity,</div><div dir="auto">Hypatia du Bois-Marie / Yutong Zhang</div><div dir="auto">Mathematician, Researcher in the Formal Sciences, (Very Annoying) Analytic Philosopher, Sinitic (Chinese) Dissident Human Rights Advocate</div><div dir="auto">Pronouns: she/they</div><div dir="auto">Cell number: +1 (845) 300-5338</div><div dir="auto">Email: <a href="mailto:knight.of.lambda.calculus@gmail.com" target="_blank" rel="noreferrer">knight.of.lambda.calculus@gmail.com</a></div></div>