Jason jcreedcmu

Let's try theorem 5 from [ACMP'25].

p ↠ p ↠ (p ∙ p)

becomes, after "constructive resource semantics" encoding,

∀α₁α₂.p @ α₁ → p @ α₂ → ∃β₁β₂(α₁α₂ = β₁β₂) × p @ β₁ × p @ β₂

or, expanded out into types, let's suppose we have

asynchronous frankenpigeon

A conlanging game for perhaps 3-5 players, suitable for a shared editable document.

All players edit a shared document.
At the top of the document is the "word bank": for each player, there is a list of between 0 and 5 words. For example, it might look like:

Alice	Bob	Carol

A conlanging game for perhaps 3-5 players, suitable for VC.

All players prepare a list of 5 made-up words, and decide on an ordering of the players.
Each player passes their word list to the next player in this order, wrapping around.
Players take turns.
On their turn, a player makes an utterance, and simultaneously tries to convey its meaning.
The utterance is in a made-up language that grows as the game goes on: the player can use words on their own list, plus any words they've already heard from other players. Using proper nouns (such as players' names) is always allowed.

This cost $5.43 This cost $3

This cost $5.43 This cost $

	import Mathlib

	class Grph (G : Type) where
	edge : G → G → Prop
	open Grph

	variable {G H : Type} [Grph G] [Grph H]

	structure Hom (G H : Type) [Grph G] [Grph H] where
	obj : G → H

	def foo : Nat := (1 + 2)
	def bar : Nat := (3 + 4)