Skip to content

Instantly share code, notes, and snippets.

View dmalikov's full-sized avatar
🥞
!

Dmitry Malikov dmalikov

🥞
!
View GitHub Profile
@ikedaisuke
ikedaisuke / gist:883394
Created March 23, 2011 16:28
reverse (reverse xs) ≡ xs in Coq
Require Import Coq.Lists.List.
Lemma rev_Unfold : forall {A:Type} (l:list A) (a:A), rev (a::l) = rev l ++ (cons a nil).
Proof.
intros.
simpl.
reflexivity.
Qed.
Theorem rev_Involutive : forall {A:Type} (l:list A), rev (rev l) = l.
@mre
mre / bitonic_sort.cu
Last active March 17, 2024 15:47
Bitonic Sort on CUDA. On a quick benchmark it was 10x faster than the CPU version.
/*
* Parallel bitonic sort using CUDA.
* Compile with
* nvcc -arch=sm_11 bitonic_sort.cu
* Based on http://www.tools-of-computing.com/tc/CS/Sorts/bitonic_sort.htm
* License: BSD 3
*/
#include <stdlib.h>
#include <stdio.h>
@copumpkin
copumpkin / State.agda
Last active October 4, 2015 15:18
The State monad
module Categories.Agda.State where
open import Categories.Category
open import Categories.Agda
open import Categories.Agda.Product
open import Categories.Functor hiding (_≡_)
open import Categories.Functor.Product
open import Categories.Functor.Hom
open import Categories.Monad
open import Categories.Adjunction
@supki
supki / hackage-authors.pl
Created June 26, 2012 20:26
Silly stuff to get hackage authors sorted by productivity.
#!/usr/bin/env perl
# This crappy perl script parses .cabal files for `authors' field and extracts authors names. Then it collects them in one enormous hash associating total number of findings. Then it "pretty"-prints hash from most productive authors to least productive.
use v5.14;
use warnings FATAL => qw(void);
# Skip all lines before /^author:/i one, then return it.
sub lex ($) {
my $h = $_[0];
while (<$h>) { if (/^author:/i) { return $_ } }
@supki
supki / udmurt.hs
Created October 16, 2012 13:08
UDMURTI SILA
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UnicodeSyntax #-}
import Data.Colour
import Diagrams.Prelude
import Diagrams.Backend.Cairo.CmdLine
import Graphics.Rendering.Diagrams.Points
main ∷ IO ()
@danchoi
danchoi / xmonad-lion.md
Created October 20, 2012 13:08
My Xmonad installation recipe for OS X Lion

My Xmonad recipe for OS X Lion

My recipe for setting up Xmonad on Ubuntu GNU/Linux is here.

What is xmonad? Read this page to learn.

Some of these instructions were adapted from the Source Matters Blog. But I also depart from those instructions in certain ways.

@copumpkin
copumpkin / Grothendieck.agda
Last active February 25, 2023 07:16
Grothendieck group
module Grothendieck where
open import Level using (_⊔_)
open import Function
open import Algebra
open import Algebra.Structures
open import Data.Product
import Relation.Binary.EqReasoning as EqReasoning
@TheEvilDev
TheEvilDev / Dependency.rb
Created November 27, 2012 00:31
Albacore improved nuspec generating, auto-dependency discovery
class Dependency
attr_accessor :Name, :Version
def initialize(name, version)
@Name = name
@Version = version
end
end
@voidlizard
voidlizard / static-linked-ghc
Created December 3, 2012 12:53
Fully statically linked haskell application
ghc -i -static -optl-static -optl-pthread -funbox-strict-fields -fwarn-incomplete-patterns -isrc --make Program.hs
@supki
supki / pemis.sml
Created February 3, 2013 18:11
proglang week 3 tests
val t1 = only_capitals [] = []
val t2 = only_capitals ["hello", "bye"] = []
val t3 = only_capitals ["Anal", "hello", "bye"] = ["Anal"]
val t4 = only_capitals ["hello", "Pemis", "bye"] = ["Pemis"]
val t5 = only_capitals ["hello", "bye", "Eblo"] = ["Eblo"]
val t6 = longest_string1 [] = ""
val t7 = longest_string1 ["pemis"] = "pemis"
val t8 = longest_string1 ["pemis", "hello"] = "pemis"
val t9 = longest_string1 ["eblo", "hello"] = "hello"