AndrasKovacs

Garbage collection with zero cost at non-GC time

Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.

I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

wenkokke

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

Gabriella439

I'm writing this post to publicly come out as trans (specifically: I wish to transition to become a woman).

This post won't be as polished or edited as my usual posts, because that's kind of the point: I'm tired of having to edit myself to make myself acceptable to others.

I'm a bit scared to let people know that I'm trans, especially because I'm not yet in a position where I can transition (for reasons I don't want to share, at least not in public) and it's really shameful. However, I'm getting really

Trebor-Huang

open import Agda.Builtin.Equality

-- Some familiar results about equality

UIP : {A : Set} (x y : A) (p q : x ≡ y) → p ≡ q
UIP x y refl refl = refl

coerce : {A : Set} (B : A → Set)
  → {x y : A} → x ≡ y
  → B x → B y

jespercockx

{-
======================================
=== THE GREAT RESURRECTION OF PROP ===
======================================

Bringing back the impredicative sort Prop of definitionally proof-irrelevant propositions to Agda.

To check this file, get the prop-rezz branch of Agda at https://github.com/jespercockx/agda/tree/prop-rezz.

This file is a short demo meant to show what you currently can (and can't) do with Prop.

bobatkey

{-# OPTIONS --rewriting #-}

module cont-cwf where

open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq

matchy233

Function Remove-DupDownloads {
    param (
        [string]$SearchPath = ".",
        [switch]$Recurse = $false
    )

    $FilePattern = '.*\([1-9][0-9]*\).*'
    $GCIParams = @{
        'Path' = $SearchPath
        'File' = $true

lambdageek

Sometimes I want to put an array inside of a mathpartir inferrule.

The straightforward thing doesn't work:

\begin{equation*}
\inferrule{Conclusion}{
  Premiss 1 \and
  \begin{array}{ll}
 1 & 2 \\ % note, this is where the problem happens

ncfavier

open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.Path.Groupoid
open import Data.Bool

data Niltok : Type where
  t : Niltok
  nicht : Niltok → Niltok
  mod2 : (n : Niltok) → n ≡ nicht (nicht n)
  coh : (n : Niltok) → ap nicht (mod2 n) ≡ mod2 (nicht n)