roboguy13

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Relation.Nullary

module MonoidNat3 where

data Expr : Set where

Lysxia

module CoDebruijn where

open import Data.Product using (_×_; _,_; ∃-syntax)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

data Context : Set where
  O : Context
  1+_ : Context → Context

data Singleton : Context → Set where

TOTBWF

(** {1 Syntax} *)

(** Expressions. *)
type expr =
  | Var of cont * int
  (** Local references.

      Thorin is a "blockless" IR, so we can reference arguments of
      other nodes by adding a data dependency edge, which implicitly
      nests the two nodes. *)

rntz

type var = string
type term = Var of var
          | Lam of var * term
          | App of term * term
          | Fix of var * term   (* only used for functions *)
          | Lit of int

type value = Int of int
           | Fun of (value -> value)

rntz

import System.Environment (getArgs)

import Control.Monad (guard, forM_)

import System.Random (RandomGen)
import qualified System.Random as Random

import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

TOTBWF

description
Inversion hell.

AndrasKovacs

Lightweight region memory management in a two-stage language

• Intro
• Basics
  • Stage inference
• Regions
  • Bit-stealing
  • Using regions
• Eager regions

atennapel

-- Polarized lambda calculus to A-normal form
-- With eta-expansion and call-saturation

type Ix = Int
type Lvl = Int

data Ty = TInt
  deriving (Show)
data TFun = TFun [Ty] Ty
  deriving (Show)

AndrasKovacs

Basic setup for formalizing elaboration

First attempts

Elaboration is, broadly speaking, taking user-written syntax and converting it to "core" syntax by filling in missing information and at the same time validating that the input is well-formed.

I haven't been fully happy with formalizations that I previously used, so I make a new attempt here. I focus on a minimal dependently typed case.

DasNaCl

Set Implicit Arguments.
Require Import List Program FunctionalExtensionality.

(** Proof of syntactic type safety for call-by-value STLC extended with ℕ. *)

(** Names/Variables will be identified with a natural number. 
    λx.λy.y x is represented as λλ0 1 *)
Definition var : Type := nat.

(** There is a need for partial maps, e.g., to keep track of what variable