[Lilug] [LILUG] formal methods that we talked about today

[Yutong Zhang]

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),

Here are the keywords I mentioned today with the microtalk about formal
methods in software:
- formal methods, software analysis, formal verification
- lambda calculus, type theory, calculus of inductive constructions, Church
encoding, Turing completeness, strong normalization, soundness
- TypeScript, PureScript, Haskell, generalized algebraic data type,
inductive data type
- structural induction, higher induction
- Gödel's second incompleteness theorem, diagonal argument, Lawvere's
fixed-point theorem
- mutability, immutability, borrow checker (rust)
- Hoare logic, separation logic
- Coq, Lean, Agda, Idris
- Verified C, Rustbelt, DeepSpec
- Satisfiability Modulo Theories, Solidity (ethereum) SMT
- Verified LLVM, Coq extraction
- BC Pierce UPenn, Thierry Coquand UGothenburg, Adam Chlipala MIT

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!

Pride and solidarity,
Hypatia du Bois-Marie / Yutong Zhang
Mathematician, Researcher in the Formal Sciences, (Very Annoying) Analytic
Philosopher, Sinitic (Chinese) Dissident Human Rights Advocate
Pronouns: she/they
Cell number: +1 (845) 300-5338
Email: knight.of.lambda.calculus at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lilug.org/pipermail/lilug-lilug.org/attachments/20230808/5e04de1d/attachment.htm>