Misc I want to read:
- Tidy Data
- The Visual Display of Quantitative Information
- Automata Theory: An Algorithmic Approach
- https://core.ac.uk/download/pdf/81980704.pdf
- Semirings, Automata, Languages
- Consistency in Dataflow Graphs
- An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
- The Marriage of Bisimulations and Kripke Logical Relations
- Decision Problems of Finite Automata Design and Related Arithmetics
- Modern Automata Theory
- Logic for Knowledge Representation, Learning, and Inference
- The Method of Coalgebra: Exercises in Coinduction
- Frames and Locales: Topology Without Points
- Twenty-One Proofs of Euler’s Formula: V-E+F=2
- Theorem Proving in Lean
- COMP3153 Algorithmic Verification — Week 2 Slides
- Inductive Approach to Spacer
- https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=9049884&tag=1
- Cell Morphing: From Array Programs to Array-Free Horn Clauses
- A SAT-Based Procedure for Verifying Finite State Machines in ACL2
- Ullman’s Subgraph Isomorphism Algorithm
- Leonora Carrington
- Buffer Placement and Sizing for High-Performance Dataflow Circuits
- Compositional Dataflow Circuits
- Verified Compilation of Synchronous Dataflow with State Machines
- A Constructive State-Based Semantics and Interpreter for a Synchronous Data-Flow Language with State Machines
- Verified Compilation of a Synchronous Dataflow Language with State Machines
- Mechanised Semantics for Gated Static Single Assignment
- Formal Verification of High-Level Synthesis
- D.B. Cooper
- CompCert – A Formally Verified Optimizing Compiler
- Eliminating Excessive Dynamism of Dataflow Circuits Using Model Checking
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- Incarnations of Burned Children
- Abstract Interpretation over Non-Deterministic Finite Tree Automata for Set-Based Analysis of Logic Programs
- https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=2d4b2164090e7a189eba740b8a4f834070e39c15
- https://ieeexplore.ieee.org/abstract/document/1348184
- https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=1b91c45edbbe85ecc3da100b962232f8b13f9a27
- Abstract Interpretation: A Semantics-Based Tool for Program Analysis
- RAHFT: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata
- Finite Presentations of Infinite Structures: Automata and Interpretations
- https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=4397326
- Fabric Tessellation: Realizing Freeform Surfaces by Smocking
- Semantics and Scheduling for Machine Knitting Compilers
- What Are the Semantics of Hardware?
- https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=5185393
- Modules — Learn You a Haskell for Great Good!
- NC-103D Instruction Manual
- Necchi EX60 Instruction Book
- Pijul, the mathematically sound version control system
- Pijul - Model
- r/math
- Monster Model
- What’s the largest finite structure you know, or…
- How monstrously long papers are made
- Interesting question related to the divergence…
- An Insecure Base: Style of Attachment and Adult Romantic Relationships
- Map of the Universe
- The Three Basic Facts of Existence: I. Impermanence (Anicca)
- Hardware Description Languages
- Abstraction, Intuition, and the “Monad Tutorial Fallacy”
- End-to-End Verification of ARM Processors with ISA-Formal
- A Dynamically Scheduled HLS Flow in MLIR
- ACL2 SV Library: SVEX-COMPILATION
- The Geometry and Topology of Three-Manifolds
- Kaluza–Klein Theory
- Nqthm, the Boyer-Moore Prover
- Learn Datalog Today!
- acl2::why-4vec-logic
- A Programmer’s Introduction to Mathematics
- Category Theory
- CpSc 513: Reading List
- Liveness Checking as Safety Checking
- My Graduate Career in Math
- Algebra - Artin
- Abstract Algebra - Benedict Gross (Harvard Extension)
- Automating Inversion of Inductive Predicates in Coq
- Verified Implementation of an Efficient Term-Rewriting Algorithm for Multiplier Verification on ACL2
- Optimized Synthesis of Sum-of-Products
- The Great Whorf Hypothesis Hoax: Sin, Suffering and Redemption in Academe
- Latency Insensitivity Testing for Dataflow HLS Designs
- Resource Sharing in Dataflow Circuits
- Embedded in Academia
- Real-Cohesive Homotopy Type Theory
- Fixing the Foundations with Semantics and Capabilities: ARM, RISC-V, and CHERI
- End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers
- End-to-End Verification of ARM Processors with ISA-Formal
- Modular Hardware Design with Timeline Types
- Rebuttal How-To: Strategies, Tactics, and the Big Picture in Research
- What Is the Relation Between a Banach Space and a Hilbert Space?
- Principles of Dependent Type Theory
- OEIS: Popcount
- feat:
grind chapter (Lean reference manual #451)
- Analysis I
- A Lean Companion to “Analysis I”
- Modal Logic for Open Minds
- the score
- point counter point
- martyr
- Apple Identity Re-Analyzed
- In search of Kazakhstan
- the bell jar
- scale - greg evans
- gulag archipelago
- Revisiting Precarity, with Care: Productive and Reproductive Labour in the Era of Flexible Capitalism
- Specified Blocks
- Lock Reasoning About While Loops
- Polytypic Proof Construction