pedagand

open import Data.Nat
open import Data.List
-- open import Data.Vec hiding (_++_)
open import Relation.Binary.PropositionalEquality

-- Vec : Set → ℕ → Set
-- Vec A n = {!!}

record LengthEq {A : Set}(l : List A)(n : ℕ) : Set where
  constructor L[_]

pedagand

import Data.Array.Accelerate
import Data.Array.Accelerate.Interpreter
import Prelude hiding ((^), (!!))
import Data.Bits

-- qr_start :: (a:u<V>32, b:u<V>32, c:u<V>32, d:u<V>32)
--      returns (aR:u<V>32, bR:u<V>32, cR:u<V>32, dR:u<V>32)
-- let
--     aR = a + b;
--     dR = (d ^ aR) <<< 16;

pedagand

import Data.Array.Accelerate
import Data.Array.Accelerate.Interpreter
import Prelude hiding ((^), (!!))
import Data.Bits

-- qr_start :: (a:u<V>32, b:u<V>32, c:u<V>32, d:u<V>32)
--      returns (aR:u<V>32, bR:u<V>32, cR:u<V>32, dR:u<V>32)
-- let
--     aR = a + b;
--     dR = (d ^ aR) <<< 16;

pedagand

Decoupling Application Logic from Persistent Memory Frameworks with AspectC++
M. Köppen, D. Friesel, C. Borchert, O. Spinczyk
https://ess.cs.uos.de/static/papers/Koeppen_2021_plos.pdf

CppSig: Extracting Type Information for C-Preprocessor Macro Expansions
C. Dietrich
https://osg.tuhh.de/Publications/2021/dietrich_21_plos.pdf

How ISO-C became unusable for operating system development
V. Yodaiken

pedagand

type ze = Z
type 'a su = S of 'a

type one = ze su
type two = ze su su
type three = ze su su su

type _ nat =
  | Ze : ze nat
  | Su : 'n nat -> 'n su nat