Ahmad Salim Al-Sibahi ahmadsalim

Center	Key People	Type	URL
Leverhume Centre for Future of Intelligence	Price - Ghahramani - Boström - Russell - Shanahan	Funding	http://lcfi.ac.uk/
Center for Human Compatible AI	Russell	Academic (UC Berkeley)	http://humancompatible.ai/
Centre for Study of Existential Risk	Price - Ó hÉigeartaigh	Academic (Cambridge)	http://cser.org/
Future of Life Institute	Tallinn - Tegmark	Funding	https://futureoflife.org
Future of Humanity Institute	Boström	Academic (Oxford)	https://www.fhi.ox.ac.uk/
OpenAI	Sutskever - Brockman	Corporate (Y Research - InfoSys - Amazon - Microsoft - Open Philantrophic Project)	https://openai.com/
AI Now Institute	Crawford - Whittaker	Academic (NYU)	https://ainowinstitute.org/
Machine Intelligence Research Institute	Soares - Yudkowsky	Corporate	https://intelligence.org/

	#lang racket/base

	(require redex/reduction-semantics
	racket/match)

	(provide (all-defined-out))

	(define-language FJ
	(P ::= (L P)
	())

	-- Inspired by https://www.fpcomplete.com/user/edwardk/phoas
	record Rec : (p : Type -> Type -> Type) -> (a : Type) -> (b : Type) -> Type where
	MkRec : (runRec : {r : Type} -> (b -> r) -> (p a r -> r) -> r) -> Rec p a b

	purerec : b -> Rec p a b
	purerec b = MkRec $ \br,_ => br b

	-- not total?
	seqrec : Rec p a b -> (b -> Rec p a c) -> Rec p a c
	seqrec m f = MkRec $ \kp, kf => runRec m (\a => runRec (f a) kp kf) kf

	-- Inspired by http://www.cse.chalmers.se/research/group/logic/AIM/AIM6/SetzerCoInduction.pdf
	{-# OPTIONS --copatterns #-}
	module Bisim where

	data ℕ : Set where
	zero : ℕ
	succ : ℕ → ℕ

	{-# BUILTIN NATURAL ℕ #-}

	module CyclicTags where

	open import Data.Colist as Col
	open import Data.Vec as V
	open import Data.Fin as F
	open import Data.Nat
	open import Data.Maybe
	open import Coinduction
	open import Data.Unit
	open import IO