brendanzab

%% Intuitionistic type theory in Twelf by Brendan Zabarauskas
%%
%% Inspired by the examples found in “An Equational Logical Framework 
%% for Type Theories” https://arxiv.org/abs/2106.01484

tp : type.
el : tp -> type.

%% Equality

kbridge

Understanding the Phases Applicative

While I was researching how to do level-order traversals of a binary tree in Haskell, I came across a library called tree-traversals which introduced a fancy Applicative instance called Phases. It took me a lot of effort to understand how it works. Although I still have some unresolved issues, I want to share my journey.

Note: I was planning to post this article on Reddit. But I gave up because it was too long so here might be a better place.

See the discussion.

Note: This article is written in a beginner-friendly way. Experts may find it tedious.

AndrasKovacs

{-# language
  BlockArguments
, ConstraintKinds
, ImplicitParams
, LambdaCase
, OverloadedStrings
, PatternSynonyms
, Strict
, UnicodeSyntax
#-}

sjoerdvisscher

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}

paul-snively

Notes on IAM (Identity and Access Management) and Zero-Trust Architecture

Overall ideas

• Pervasive X.509 authentication with SPIFFE standards using the SPIRE reference implementation
• Frequent (e.g. hourly) rotation of dynamically-generated certificates for mTLS between nodes/workloads in the usual SPIFFE way
• In Kubernetes:
  • cert-manager with csi-driver-spiffe
  • k8s Workload Registrar — deprecated in favor of the spire-controller-manager
• Most workloads will use csi-driver-spiffe as described here to provide the SPIFFE_ENDPOINT_SOCKET evironment variable and the [Java SPIFFE Provider](https://github.com/spiffe/java-spiffe/blob/main/java-spiffe-provider/R

wilbowma

open import Data.Nat
open import Data.Bool hiding (_<_)
open import Data.List
open import Data.Fin hiding (_<_; _+_)
open import Data.Unit
open import Relation.Nullary
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- What is a semantics? A semantics defines the meaning of terms.

AndrasKovacs

{-# OPTIONS --prop --without-K --show-irrelevant --safe #-}

{-
Challenge:
- Define a deeply embedded faithfully represented syntax of a dependently typed
  TT in Agda.
- Use an Agda fragment which has canonicity. This means that the combination of
  indexed inductive types & cubical equality is not allowed!
- Prove consistency.

AndrasKovacs

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.

andrejbauer

{- Here is a short demonstration on how to use Agda's solvers that automatically
   prove equations. It seems quite impossible to find complete worked examples
   of how Agda solvers are used.

   Thanks go to @anormalform who helped out with these on Twitter, see
   https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng

   I welcome improvements and additions to this file.

   This file works with Agda 2.6.2.2 and standard-library-1.7.1

odomanov

-- Automatic derivation of equality for inductive types. Examples.
-- Inspired by https://github.com/alhassy/gentle-intro-to-reflection.
-- Tested on: Agda version 2.6.2.1-59c7944, std-lib 1.7

module _ where

open import Data.Bool
open import Data.List
open import Data.Unit
open import Relation.Binary.PropositionalEquality