mietek

{-

McBride, C. (2010) “Djinn, monotonic”
http://www.easychair.org/publications/download/Djinn_Monotonic

-}

module Memo where

open import Data.Nat using (ℕ ; zero ; suc)

mietek

{-# OPTIONS --rewriting #-}

-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Gentzen-style formalisation of syntax with context pairs, after Pfenning-Davies.
-- Normal forms, neutrals, and spines.

module BasicIS4.Syntax.DyadicGentzenSpinalNormalForm where

open import BasicIS4.Syntax.DyadicGentzen public

mietek

module Foo where


open import Data.Nat public
  using (ℕ ; zero ; suc ; _≟_)

open import Relation.Binary.PropositionalEquality public
  using (_≡_ ; _≢_ ; refl ; trans ; sym ; cong ; cong₂ ; subst)

open import Relation.Binary.HeterogeneousEquality public

mietek

cut′ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ B
cut′ t u = [ top ≔ t ] u

mcut′ : ∀ {A B Γ Δ} → ∅ ⁏ Δ ⊢ A → Γ ⁏ Δ , A ⊢ B → Γ ⁏ Δ ⊢ B
mcut′ t u = m[ top ≔ t ] u

extend : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → Γ , A ⁏ Δ ⊢⋆ Ξ , A
extend {∅}     ∙        = ∙ , v₀
extend {Ξ , B} (ts , t) = mono⊢⋆ weak⊆ ts , mono⊢ weak⊆ t , v₀

mietek

diff --git a/BasicT/Syntax/Gentzen.agda b/BasicT/Syntax/Gentzen.agda
index 181fdf6..fadeb4d 100644
--- a/BasicT/Syntax/Gentzen.agda
+++ b/BasicT/Syntax/Gentzen.agda
@@ -23,8 +23,8 @@ data _⊢_ (Γ : Cx Ty) : Ty → Set where
   if    : ∀ {C}   → Γ ⊢ BOOL → Γ ⊢ C → Γ ⊢ C → Γ ⊢ C
   zero  : Γ ⊢ NAT
   suc   : Γ ⊢ NAT → Γ ⊢ NAT
-  it    : ∀ {C}   → Γ ⊢ NAT → Γ ⊢ C ▻ C → Γ ⊢ C → Γ ⊢ C
-  rec   : ∀ {C}   → Γ ⊢ NAT → Γ ⊢ NAT ▻ C ▻ C → Γ ⊢ C → Γ ⊢ C

mietek

data Nat : Set where

postulate
  Foo : Nat → Set

data Bar₁ : (n : Nat) → Foo n → Set where
data Bar₂ : ∀ (n : Nat) → Foo n → Set where
data Bar₃ : ∀ n → Foo n → Set where
-- NOPE: data Bar₄ : n → Foo n → Set where

mietek

module GentzenSystemT where

open import Agda.Primitive public
  using ()
  renaming (_⊔_ to _⊔ˡ_ ; lsuc to sucˡ)

open import Data.Nat public
  using (ℕ ; zero ; suc)
  renaming (_≟_ to _≟ᴺ_)

mietek

module BasicICML.Syntax.Experiment3 where

open import Common.Context public


mutual
  infixl 8 _∧_
  infixr 6 _▻_
  data Ty : Set where
    α_  : Atom → Ty

mietek

-- Gentzen-style formalisation of syntax with context pairs, after Nanevski-Pfenning-Pientka.

module BasicICML.Syntax.DyadicGentzen where

open import Common.Context public


mutual
  infixr 9 [_]_
  infixl 8 _∧_

mietek

{-

Normalisation by evaluation for LP,
with types parametrised by closed typed derivations,
Hilbert-style syntax, and glueing-style semantics.

NOTE: The definition of forcing is questionable.

-}