Ahmad Salim Al-Sibahi ahmadsalim

## ai-research.csv

          
            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/

## FJ.rkt
#lang racket/base

(require redex/reduction-semantics
         racket/match)

(provide (all-defined-out))

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

## phoas.idr
-- 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

## Bisim.agda
-- 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 ℕ #-}

## CyclicTags.agda
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
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