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 

jake-87

A somewhat brief overview of typechecking System F

This document comprises an example of typechecking a type system based on System F, in a small ML-like language.

You can skip the below section if you already understand System F itself.

A brief overview of System F

System F is the name given to an extension of the simply typed lambda calclus.

ncfavier

-- Moved to https://agda.monade.li/Goat.html

AndrasKovacs

{-# OPTIONS --without-K #-}

-- version 1, conversion is indexed over conversion
module IndexedConv where

  data Con  : Set
  data Ty   : Con → Set
  data Sub  : Con → Con → Set
  data Tm   : ∀ Γ → Ty Γ → Set
  data Con~ : Con → Con → Set

wilbowma

{-# OPTIONS --guarded #-}


open import Agda.Primitive
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; sym; trans)
open import Data.Unit using (⊤; tt)
open import Data.Nat -- using (ℕ; _+_; suc; _<_)
open import Data.Nat.Properties
open import Data.Fin using (Fin; fromℕ; fromℕ<)
open import Data.Vec using (Vec; lookup; []; _∷_; [_]; _++_; map)