{{ message }}

Instantly share code, notes, and snippets.

# Benbmsherman

Created Mar 21, 2019
Computable semantics of random streams
View StreamSemantics.asd
 ! Standard operations let tt : bool = mkbool True False;; let ff : bool = mkbool False True;; let log (x : real) : real = dedekind_cut (fun q : real => exp q 0.5 right cos q < 0.5);; let pi : real = cut q : [3.1415926, 3.1415927] left sin q > 0 right sin q < 0;; let twopi : real = cut q : [6.28318, 6.28319] left sin q < 0 right sin q > 0;;
Created Aug 2, 2016
View Refine.v
 (* Categories *) Class Cat {C : Type} := { arr : C -> C -> Type ; eq : forall {A B : C}, arr A B -> arr A B -> Prop }. Arguments Cat : clear implicits. Section Functor. Context {C D : Type} `{Cat C} `{Cat D}.
Created May 28, 2016
Coq's classical real numbers imply the weak law of excluded middle
View RealLEM.v
 Require Import Reals. Definition WeakLEM := forall (P : Prop), {~~P} + {~P}. Local Open Scope R_scope. Definition ind (P : Prop) (x : R) : Prop := (x = 0) \/ (x = 1 /\ P).
Created May 18, 2016
Semideciders
View Semideciders.v
 CoInductive Partial {A : Type} : Type := | Now : A -> Partial | Later : Partial -> Partial. Arguments Partial : clear implicits. (** We can use this to loop. *) CoFixpoint loop {A : Type} := @Later A loop. Definition unfold_Partial {A : Type} : forall (px : Partial A),
Created Mar 28, 2016
An isomorphism of types involving truncation.
View InhabitedIso.v
 Record T { A B : Type } : Type := { to : A -> B ; from : B -> A ; from_to : forall (a : A), from (to a) = a ; to_from : forall (b : B), to (from b) = b }. Arguments T : clear implicits. Inductive inhabited {A : Type} : Prop :=
Created Jan 6, 2016
Tree indices
View Tree_indices.v
 Inductive Tree := | Branch : forall {n}, Vector.t Tree n -> Tree. Inductive TreeNode : Tree -> Type := | Root : forall {t : Tree}, TreeNode t | InBranch : forall {n : nat} {xs : Vector.t Tree n} (i : Fin.t n), TreeNode (Vector.nth xs i) -> TreeNode (Branch xs). Lemma fin_dec : forall {n : nat} (x y : Fin.t n),
Last active Dec 31, 2015
View Sampler.hs
 {-# LANGUAGE Rank2Types #-} module Sampler where import Control.Applicative import System.Random data Sampler a = Sampler { sample :: RandomGen g => g -> (a, g) } instance Monad Sampler where (Sampler f) >>= g = Sampler \$ \r -> let (x, r2) = f r; Sampler h = g x in h r2
Created Nov 6, 2013
Results from summing a vector of length n with constant 1s using accelerate for values of n ranging from 1 to 1025. Left: interpreter, Right: CUDA.
View cuda-fold-failures
 Intrp. CUDA 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9
Created Nov 6, 2013
CUDA device query
View device-query
 ./deviceQuery Starting... CUDA Device Query (Runtime API) version (CUDART static linking) Detected 1 CUDA Capable device(s) Device 0: "GeForce GTX 580" CUDA Driver Version / Runtime Version 5.5 / 5.5 CUDA Capability Major/Minor version number: 2.0 Total amount of global memory: 3072 MBytes (3220766720 bytes)
Created Nov 6, 2013
Output of running accelerate-examples --cuda -k There are failures.
View accelerate-examples-cuda-failure
 running with CUDA backend to display available options, rerun with '--help' map-abs: Ok map-plus: Ok map-square: Ok zip: Ok zipWith-plus: Ok fold-sum: Ok fold-product: Ok
You can’t perform that action at this time.