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.

anuyts

Equality-in-equality-out category theory in cubical Agda

Now that equality has become computationally relevant but composition of equality remains cumbersome, the statement of various equality laws in the cubical library feels "wrong". Here I want to explore an alternative approach.

What I'm not proposing

To avoid confusion, I want to start by emphasizing what I'm not proposing.

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