Dominic Orchard dorchard

My (partial and personal) notes from ESOP 2021.

Disclaimer: There may well be errors and omissions here, so please do read the original papers instead of relying on my notes! Apologies to the author's for any misrepresentation. Due to other pressures I am not able to take notes on all the talks, and some notes are partial.

Session 1 - Probabilistic Programming and Verification (Chaired by Sam Staton)

Automated Termination Analysis of Polynomial Probabilistic Programs - Marcel Moosbrugger et al.

Whilst using the Ott tool for defining programming languages and semantics (http://www.cl.cam.ac.uk/~pes20/ott/) I have noticed that I sometimes get the following error when compiling its generated LaTeX:

  ! LaTeX Error: Too many math alphabets used in version normal.

This is a difficult to track down error (but also mildly amusing)! Here are the solutions/reasons I've found so far:

Using pdflatex? Try switching to xelatex which can support up 256 math fonts.

(by Dominic Orchard, School of Computing, University of Kent, 2018)

Disclaimer: this advice is non exhaustive, and every piece of advice might not suit you. At least, I hope it helps you to think about how you can develop your own strategy for exam preparation.

My top tip is to see exams as formative rather than purely about assessment. This is an opportunity to force yourself to learn a topic deeply, which will then benefit you in the future, rather than a box ticking exercise to get a fancy piece of paper at the end. This will orient your attitude to maximising your potential.

Exams are hard. They occupy a short space of time in your whole life but they can have a big impact on the rest of it, so make the most of them. Study well and study wisely.

	module Main where

	import System.Environment (getArgs)
	import System.Exit (exitFailure)
	import Data.List (intercalate)

	-- Scrub automata
	scrub :: String -> [String]
	scrub [] = []
	scrub ('m':'a':'i':'l':'t':'o':':':rest) =

	module Empty where

	open import Data.Empty
	open import Relation.Binary.PropositionalEquality
	open import Relation.Nullary
	open import Function.Inverse

	-- Empty type has only unequal elements
	uneq : (x y : ⊥) -> x ≢ y
	uneq () y prf

	# Sonic Pi code used in the intro of my talk on
	# "Effect Systems Revisited — Control-Flow Algebra and Semantics" (Mycroft, Orchard, Petricek)
	# https://kar.kent.ac.uk/61623/1/effects-revisited.pdf
	# for Hanne and Flemming Nielson's Festschrift, January 2016.

	# Not the prettiest or most modern SonicPi code!

	use_transpose(6)
	use_bpm(146)
	use_synth :piano

	module OrdersAndEquivClasses where

	open import Level
	open import Data.Product

	-- X is the base
	-- S is a set of things drawn from X
	record PreOrder {l l' : Level} {X : Set l} {S : X -> Set l'} : Set (Level.suc l ⊔ l') where
	field
	_<_ : Σ X S -> Σ X S -> Set l

	\documentclass[a4paper]{article}

	\usepackage[table,x11names]{xcolor}
	\usepackage{afterpage}
	\usepackage{colortbl}
	\usepackage{forloop}
	\usepackage{geometry}

	\begin{document}

	'.source.idris':
	'∞':
	'prefix': 'Inf'
	'body': '∞'

	'.source.haskell':
	'∞':
	'prefix': 'Inf'
	'body': '∞'

	#!/bin/bash
	cp ~/template.tex paper.tex

Dominic Orchard dorchard

Session 1 - Probabilistic Programming and Verification (Chaired by Sam Staton)

Automated Termination Analysis of Polynomial Probabilistic Programs - Marcel Moosbrugger et al.

Exam preparation