vault backup: 2025-02-25 15:33:34

2 Cole Group Meeting Notes/Weekly Note 2025-02-25.md

@@ -14,6 +14,20 @@ tags: []
 # Last Week's Plan
 # Accomplishments
 ## Remarks
+### A Myriad of Programming Language Learning
+1. Haskell - Did first two chapters of the book. Learned all about set building with predicates, and I'm pretty impressed. The Haskell book made a good point about trimming down solutions, additive vs subtractive manufacturing
+2. Lean - I have proved 2+2=4. Successfully explained it to my girlfriend, who hates programming.
+3. TLA+ - Watched the first two video lectures. I also got my own set up for writing TLA instead of using the TLA Toolbox. The next video I need to watch is Lamport telling me why I need to use the TLA Toolbox. 
+### Reading
+I've not been learning to write Assembly, but I have been learning about it. 
+I've read a bit of paper on verifying Assembly code
+### Classes
+1. ME 2150 - Did microkit part 3 and part 4. Wasn't too bad. Turns out I suck at wordle with 5 tries instead of 6 though. 
+2. NUCE 2113 - Laboratory 5 - Doing radiation spectrums using sodium iodide detectors
+3. ME 2046 - Learned about the w plane. An interesting idea that seems so simple of doing with the inverse of tustin's transform.
+### Service
+GSA - taught some qualifying exam takers about the state of the art. 
+Poked Antoine about NUCE classes for the summer, also chatted with Gleeson. Need to email them both.
 ## Tasks and Notes From This Past Week
 >[!abstract] Read Papers
 >```tasks

201 Metadata/My Library.bib

@@ -4518,6 +4518,22 @@ Artificial Intelligence Program.pdf}
   isbn = {0-262-35100-5}
 }
 
+@article{fromherzVerifiedEfficientEmbedding2019,
+  title = {A Verified, Efficient Embedding of a Verifiable Assembly Language},
+  author = {Fromherz, Aymeric and Giannarakis, Nick and Hawblitzel, Chris and Parno, Bryan and Rastogi, Aseem and Swamy, Nikhil},
+  date = {2019-01-02},
+  journaltitle = {Source code for Article: A Verified, Efficient Embedding of A Verifiable Assembly Language},
+  shortjournal = {Proc. ACM Program. Lang.},
+  volume = {3},
+  pages = {63:1--63:30},
+  doi = {10.1145/3290376},
+  url = {https://dl.acm.org/doi/10.1145/3290376},
+  urldate = {2025-02-14},
+  abstract = {High-performance cryptographic libraries often mix code written in a high-level language with code written in assembly. To support formally verifying the correctness and security of such hybrid programs, this paper presents an embedding of a subset of x64 assembly language in F* that allows efficient verification of both assembly and its interoperation with C code generated from F*. The key idea is to use the computational power of a dependent type system's type checker to run a verified verification-condition generator during type checking. This allows the embedding to customize the verification condition sent by the type checker to an SMT solver. By combining our proof-by-reflection style with SMT solving, we demonstrate improved automation for proving the correctness of assembly-language code. This approach has allowed us to complete the first-ever proof of correctness of an optimized implementation of AES-GCM, a cryptographic routine used by 90\% of secure Internet traffic.},
+  issue = {POPL},
+  file = {/home/danesabo/Zotero/storage/JAJSQPC2/Fromherz et al. - 2019 - A verified, efficient embedding of a verifiable assembly language.pdf}
+}
+
 @inproceedings{fultonKeYmaeraAxiomaticTactical2015,
   title = {{{KeYmaera~X}}: {{An Axiomatic Tactical Theorem Prover}} for {{Hybrid Systems}}},
   shorttitle = {{{KeYmaera~X}}},