Yazalde Filimone yazaldefilimone

Locate the section for your github remote in the .git/config file. It looks like this:

[remote "origin"]
	fetch = +refs/heads/*:refs/remotes/origin/*
	url = [email protected]:joyent/node.git

Now add the line fetch = +refs/pull/*/head:refs/remotes/origin/pr/* to this section. Obviously, change the github url to match your project's URL. It ends up looking like this:

Achieving warp speed with Rust

Books

A list of links containing cool references, resources and things related to books about Computer Science and related.

Haskell Programming for First Principles
Types and Programming Languages #math/type-theory
Essentials of Compilation #computer-science/compilers
How to design computer programs
Structure and Interpretation of Computer Programs
Introduction to Theory of Computation, Michael Sipser #computer-science/theory-of-computation

ported from https://hub.darcs.net/dolio/agda-share/browse/PHOASNorm.agda

JS

const Lam = bod => lam => app => vah => lam(bod);
const App = fun => arg => lam => app => vah => app(fun)(arg);
const Var = exp => lam => app => vah => vah(exp);

const nz = v => nz => ns => nz(v);

Can a simple functional sieve be fast? Optimizing Tromp's algorithm on HVM.

Today, John Tromp - creator of the Binary λ-Calculus, and one of the smartest functional wizards alive - ported his famous prime number generator (first published 12 years ago!) to HVM:

Solving SAT via interaction net superpositions

I've recently been amazed, if not mind-blown, by how a very simple, "one-line" SAT solver on Interaction Nets can outperform brute-force by orders of magnitude by exploiting "superposed booleans" and optimal evaluation of λ-expressions. In this brief note, I'll provide some background for you to understand how this works, and then I'll present a simple code you can run in your own computer to observe and replicate this effect. Note this is a new observation, so I know little about how this algorithm behaves asymptotically, but I find it quite



	ast.exe: ast.c
	gcc -Werror -Wswitch -Wimplicit-fallthrough ast.c -o ast.exe

	clean:
	rm -f .o .exe *.s a.out

	test.s: ast.exe
	./ast.exe > test.s

	impl<V: Value> core::str::FromStr for NonNormalizingDec<V> {
	type Err = &'static str;

	#[inline(never)]
	#[rustfmt::skip]
	fn from_str(s: &str) -> Result<Self, Self::Err> {
	/// Converts an ASCII decimal digit to an int.
	///
	/// In release builds, no range checks are performed and passing a
	/// non-digit character will result is undefined (yet safe) behavior.

	{-# OPTIONS --copatterns #-}

	module UntypedLambda where

	open import Size
	open import Function

	mutual

	data Delay (A : Set) (i : Size) : Set where

	// A nano dependent type-checker featuring inductive types via self encodings.
	// All computation rules are justified by interaction combinator semantics,
	// resulting in major simplifications and improvements over old Kind-Core.
	// Specifically, computable annotations (ANNs) and their counterpart (ANN
	// binders) and a new self encoding based on equality (rather than dependent
	// motives) greatly reduce code size. A more complete file, including
	// superpositions (for optimal unification) is available on the
	// Interaction-Type-Theory repository.
	// Credits also to Franchu and T6 for insights.

Yazalde Filimone yazaldefilimone

Achieving warp speed with Rust

Contents:

Books

Can a simple functional sieve be fast? Optimizing Tromp's algorithm on HVM.

Solving SAT via interaction net superpositions