dorchard

from typing import TYPE_CHECKING

flag : bool = True

def greet(name: str) -> None:
   """Say hello to everyone"""
   print("Hi " + name)
   return None

greet("Manchester")

dorchard

import Data.Bits
import Data.Word
import Foreign ( Ptr, new, castPtr, Storable(peek, poke) )
import System.IO.Unsafe
import Unsafe.Coerce

qsqrt :: Float -> Float
qsqrt x = 1 / qRsqrt x

qsqrt' :: Float -> Float

dorchard

\documentclass[10pt]{article}
\usepackage{amssymb} %maths
\usepackage{amsmath} %maths
\usepackage[utf8]{inputenc} %useful to type directly diacritic characters
\usepackage[margin=4cm]{geometry}

\title{Indexed natural numbers}
\author{Dominic Orchard}

\begin{document}

dorchard

program example
  use naryfunc
  implicit none
  ! Outputs 2 6 24
  write(*,*) mult(2), mult(2, 3), mult(2, 3, 4)
end program example

dorchard

module Flexible where

-- Exploring flexible graded monads, based on the work of Katsumata, McDermott, Uustalu and Wu
-- https://dylanm.org/drafts/flexibly-graded-presentations.pdf

open import Function

_⇒_ : {E : Set} -> (E -> Set) -> (E -> Set) -> Set
_⇒_ {E} X Y = forall (e : E) -> X e -> Y e

dorchard

-- # Examples from the paper 'Linearity and Uniqueness: An Entente Cordiale'

-- ## Linearity (see Section 2, Key ideas)

-- Linearity (with cake)

data Cake  = Cake
data Happy = Happy

eat : Cake -> Happy

dorchard

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) =

dorchard

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

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.

dorchard

# 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