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

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

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

TOOL := main.exe


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

.DEFAULT_GOAL := all

all: clean run

jtpaasch

TOOL := main.exe


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

.DEFAULT_GOAL := all

all: clean run

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

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

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

Relational Verification

Beckert, B. and M. Ulbrich. (2018) "Trends in Relational Program Verification." In I. Schaefer and P. Muller (Eds.), Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of His 60th Birthday. Springer, pp. 41-58.

Relational verification verifies relational properties that relate different programs.

To verify relational properties, one must (in principle) compare several runs of the same program.

Some examples of relational properties:

jtpaasch

-- This version of fold applies 'f' to the head of the list '[a]' 
-- to get a new accumulation 'acc', then it recurses into the tail
-- of the list '[a]' where it then repeats. This means that the
-- accumulated results are built up by adding in the elements 
-- of the list, one at a time, starting with the first element 
-- (on the left), and then moving through them, going right.
foldLeft :: (b -> a -> b) -> b -> [a] -> b
foldLeft f acc xs =
  case xs of
    [] -> acc