- https://www.ccs.neu.edu/home/amal/papers/seminterop.pdf
- https://arxiv.org/pdf/1711.03871.pdf
- https://lamport.azurewebsites.net/pubs/hyper2.pdf
- https://arxiv.org/pdf/2106.02628.pdf
- https://www-sop.inria.fr/everest/Tamara.Rezk/publication/Barthe-DArgenio-Rezk-Journal.pdf
- https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=7536379
JT Paasch jtpaasch
jtpaasch
/ Specification-Synthesis-Notes.md
Last active
October 11, 2022 16:22
Some notes on literature on spec synthesis.
These notes explain how a linker works and how to write a linker script. It is very basic, but the goal is to illuminate how it works in the simplest possible way.
The linker for most Linux systems is ld, which has a default linker script. To see the default linker script:
ld --verbose
To specify a custom linker script:
jtpaasch
/ CS-Papers.md
Last active
August 13, 2022 15:01
A list of papers in programming languages and CS that I want to check out
- Klebenov et al, Automating Regression Verification of Pointer Programs by Predicate Abstraction. https://formal.kastel.kit.edu/~ulbrich/pdf/FMSD2017.pdf [I've read this]
Differential program analysis (relational equivalence)
- Zachs and Pnueli, The "Cross-Product Program" paper. https://llvm.org/pubs/2008-05-CoVaC.pdf
- Barthes et al. Relational Verification using Product Programs.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| TOOL := main.exe | |
| ##################################################### | |
| # DEFAULT | |
| ##################################################### | |
| .DEFAULT_GOAL := all | |
| all: clean run |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| TOOL := main.exe | |
| ##################################################### | |
| # DEFAULT | |
| ##################################################### | |
| .DEFAULT_GOAL := all | |
| all: clean run |
A Heyting algebra is a bicartesian closed poset. I.e.,
- It has a greatest element 1 (top, true)
- It has a least element 0 (bottom, false)
- It has all meets (intersections, products, logical "and")
- It has all joins (unions, coproducts, sums, logical "or")
- It has all horseshoes (internalized implications, exponentials, the material conditional)
jtpaasch
/ Setting-up-editors-for-OCaml.md
Last active
February 16, 2022 17:23
Notes on setting up emacs/vim for OCaml
jtpaasch
/ Modalities-Notes.md
Last active
January 22, 2022 15:40
Notes on modalities in category theory and type theory
- Mitchell, Foundations, section 7.3 (Kripke Lambda Models)
- Ranta, article on possible worlds
- Bell, Topos: Local Set Theories
- Goldblatt, Mathematics of Modality chapters on modality
- nLab on categories of contexts (syntactic categories)
- Taylor, Practical Foundations, chapter on CCCs has stuff on categories of contexts
- Emily Reihl's video lecture on monads and Lawere theories
- Primiero on information
jtpaasch
/ Category-Theory.md
Last active
June 1, 2024 17:06
Notes, resources, etc on category theory