Alexandre Moreno moleike

🌟

dare to think for yourself

moleike / App.java

Created April 28, 2020 10:03 — forked from thomasdarimont/App.java

Simple AuthN & AuthZ example with Spring Boot / Security / Session

	package demo;

	import java.io.Serializable;
	import java.security.Principal;
	import java.util.Collection;
	import java.util.Collections;
	import java.util.HashMap;
	import java.util.Map;
	import java.util.UUID;

moleike / CC.hs

Created July 4, 2020 06:17 — forked from atennapel/CC.hs

Calculus of Constructions, normalization-by-evaluation, semantic typechecking

	data Tm = Var Int \| Ann Tm Tm \| Abs Tm \| App Tm Tm \| Pi Tm Tm \| Fix Tm \| Uni
	data Clos = Clos Tm Env
	data Dm = DVar Int \| DAbs Clos \| DNeutral Int [Dm] \| DPi Dm Clos \| DFix Clos \| DUni
	type Env = [Dm]

	capp :: Clos -> Dm -> Dm
	capp (Clos b e) t = eval (t : e) b

	vapp :: Dm -> Dm -> Dm
	vapp a b =

moleike / benchmark.md

Created March 29, 2021 02:19 — forked from CertainLach/benchmark.md

Jrsonnet performance

Benchmark results

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
`jrsonnet large_string_join.jsonnet`	16.5 ± 0.5	16.1	19.6	1.00
`gojsonnet large_string_join.jsonnet`	90.7 ± 3.8	85.6	104.0	5.49 ± 0.29
`jsonnet large_string_join.jsonnet`	69.5 ± 2.4	68.2	78.1	4.20 ± 0.20
`sjsonnet large_string_join.jsonnet`	760.6 ± 12.7	739.9	787.2	46.00 ± 1.67

moleike / closconv.lhs

Created June 5, 2021 01:41 — forked from jozefg/closconv.lhs

Tutorial on Closure Conversion and Lambda Lifting

	This is my short-ish tutorial on how to implement closures in
	a simple functional language: Foo.

	First, some boilerplate.

	> {-# LANGUAGE DeriveFunctor, TypeFamilies #-}
	> import Control.Applicative
	> import Control.Monad.Gen
	> import Control.Monad.Writer
	> import Data.Functor.Foldable

moleike / cantor.agda

Created April 25, 2025 15:30 — forked from jozefg/cantor.agda

A generalization of Cantor's diagonalization argument.

	module cantor where
	open import Data.Product
	open import Data.Empty
	open import Level

	-- A variant of (https://coq.inria.fr/refman/language/core/inductive.html?highlight=cantor)

	-- Sort of spooky this works.
	data _≡_ {ℓ : Level}{A : Set ℓ} : A → A → Set₀ where
	refl : (a : A) → a ≡ a