jtpaasch

Specification Synthesis

To Read

• 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

jtpaasch

How Linkers Work

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 (PL mostly)

• 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.

jtpaasch

TOOL := main.exe


#####################################################
# DEFAULT
#####################################################

.DEFAULT_GOAL := all

all: clean run

jtpaasch

TOOL := main.exe


#####################################################
# DEFAULT
#####################################################

.DEFAULT_GOAL := all

all: clean run

jtpaasch

Heyting Algebras

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

Setting up the package manager - emacs

Add this to .emacs:

(require 'package)
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/"))

jtpaasch

Modalities

• 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 Notes

Resources

• https://boris-marinov.github.io/category-theory-illustrated/

• https://markkarpov.com/post/category-theory-part-1.html

• https://medium.com/sadasant/sections-and-retractions-a1a30601c000

jtpaasch

ARM Assembly

Tutorials

• https://runestone.academy/runestone/books/published/armTutorial/index.html
• https://azeria-labs.com/writing-arm-assembly-part-1/

Filenames