MaskRay

theme	class	highlighter	fonts
default	text-center	MaskRay	sans serif mono sans-serif serif monospace

p4bl0-

This project is a tiny compiler for a very simple language consisting of boolean expression.

The language has two constants: 1 for true and 0 for false, and 4 logic gates: ! (not), & (and), | (or), and ^ (xor).

It can also use parentheses to manage priorities.

Here is its grammar in BNF format:

expr ::= "0" | "1"

codyroux

Confluence. It's not just a place where you can complain about colleagues to other colleagues.

It's also a property that is quite useful in many areas of CS!

As a reminder, a (non-deterministic) reduction relation --> is confluent if for every (multi-step) "peak" u *<-- t -->* v (I use -->* for the multi-step version of -->) there is a corresponding "valley": u -->* w *<-- v.

This basically says that your computation can't be "too"

gbaz

This post will discuss how to model Simplicial Sets (sSets) in Haskell, using their category-theoretic definition.

Introduction

If you want to know what these are, a good primer is Friedman's introduction to simplicial sets. Another, more concrete perspective is provided by Sergeraert's introduction to combinatorial homotopy theory

Now why would we want to model this thing anyway, and why are we going to jump through categorical hoops to do so?

Well, we want to model sSets because they are a basic way in which people carry out homotopy theory, which in turn is about reducing the class of spaces (or shapes, if you prefer) into spaces modulo their continuous transformations into one another, thus giving us a way to talk about shapes/spaces ""in general"". Now in turn we need to represent shapes/spaces in a concrete way, and we do so by identifying them with certain decompositions of them

lexi-lambda

Monads and delimited control are very closely related, so it isn’t too hard to understand them in terms of one another. From a monadic point of view, the big idea is that if you have the computation m >>= f, then f is m’s continuation. It’s the function that is called with m’s result to continue execution after m returns.

If you have a long chain of binds, the continuation is just the composition of all of them. So, for example, if you have

m >>= f >>= g >>= h

then the continuation of m is f >=> g >=> h. Likewise, the continuation of m >>= f is g >=> h.

sam-lb

# I am ashamed for writing this.
import inspect;

class Cin:

    """ time to whip out some python magic """

    def __rshift__(self, other):
        # I don't want to require that "other" is declared global.
        cin = input();

MattPD

Program Analysis Resources

(draft; work in progress)

See also:

• Compilers
  • correctness
• Program analysis:
• Dynamic analysis - instrumentation, translation, sanitizers

danidiaz

A series of reading lists mostly related to functional programming.

edsko

(* Developed using Coq 8.4pl5 *)

Require Import Coq.Setoids.Setoid.
Require Import Coq.Logic.ProofIrrelevance.
Require Import Coq.Logic.JMeq.

Set Implicit Arguments.

(* Auxiliary *)

chrisdone

Basic unit type:

λ> replTy "()"
() :: ()

Basic functions: