Imagen de Portada

Abstraction Functions as Types

Fuente: Zenodo

Guardado en:

Detalles Bibliográficos
Autores principales:	Grodin, Harrison, Li, Runming, Harper, Robert
Formato:	Recurso digital
Publicado:	Zenodo 2025
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

_version_	1866902136841830400
author	Grodin, Harrison Li, Runming Harper, Robert
author_facet	Grodin, Harrison Li, Runming Harper, Robert
contents	<p><strong>Abstraction Functions as Types</strong></p> <p>This repository contains a Cubical Agda formalization of the queue examples and a corresponding library of phase primitives and lemmas from the paper “Abstraction Functions as Types”.</p> <p><strong>List of claims</strong></p> <table style="width: 79.773157%; height: 14px; border-collapse: collapse; border-spacing: 0px; border-width: 1px; margin-left: 0px; margin-right: auto;"> <tbody> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p><strong>Section</strong></p> <p> </p> </td> <td style="width: 21.593918%; height: 80px;"> <p><strong>Item</strong></p> <p> </p> </td> <td style="width: 15.183867%; height: 80px;"> <p><strong>File</strong></p> <p> </p> </td> <td style="width: 23.96204%; height: 80px;"> <p><strong>Name</strong></p> <p> </p> </td> <td style="width: 29.537367%; height: 80px;"> <p><strong>Notes</strong></p> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Definition 2.1</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>◯</code></p> </td> <td style="width: 29.537367%; height: 80px;"> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Definition 2.2</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Concrete</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>●</code></p> </td> <td style="width: 29.537367%; height: 80px;"> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Lemma 2.3</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>isConcrete</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p>by definition</p> </td> </tr> <tr style="height: 99px;"> <td style="width: 9.604184%; height: 99px;"> <p>§2.1.1</p> </td> <td style="width: 21.593918%; height: 99px;"> <p>Semantics 1</p> </td> <td style="width: 15.183867%; height: 99px;"> <p>Semantics.Abstract</p> </td> <td style="width: 23.96204%; height: 99px;"> <p><code>◯-semantics</code> and <code>●-semantics</code></p> </td> <td style="width: 29.537367%; height: 99px;"> </td> </tr> <tr style="height: 99px;"> <td style="width: 9.604184%; height: 99px;"> <p>§2.1.1</p> </td> <td style="width: 21.593918%; height: 99px;"> <p>Semantics 2</p> </td> <td style="width: 15.183867%; height: 99px;"> <p>Semantics.Concrete</p> </td> <td style="width: 23.96204%; height: 99px;"> <p><code>◯-semantics</code> and <code>●-semantics</code></p> </td> <td style="width: 29.537367%; height: 99px;"> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.1.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Glue</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Glue</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>Glue'</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p>applies modalities, for convenience</p> </td> </tr> <tr style="height: 99px;"> <td style="width: 9.604184%; height: 99px;"> <p>§2.1.2</p> </td> <td style="width: 21.593918%; height: 99px;"> <p>Theorem 2.4</p> </td> <td style="width: 15.183867%; height: 99px;"> <p>Modality.Glue</p> </td> <td style="width: 23.96204%; height: 99px;"> <p><code>glue</code></p> </td> <td style="width: 29.537367%; height: 99px;"> <p>only defining one of the involved maps</p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.2.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>PreQueue</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Queue.Base</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>PreQueue</code></p> </td> <td style="width: 29.537367%; height: 80px;"> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.2.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p><em>X</em>, empty, enqueue, dequeue</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Queue.Glued</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>batchedPreQueue</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 99px;"> <td style="width: 9.604184%; height: 99px;"> <p>§2.3.1</p> </td> <td style="width: 21.593918%; height: 99px;"> <p>Batch, empty, enqueue, dequeue</p> </td> <td style="width: 15.183867%; height: 99px;"> <p>Queue.Quotient</p> </td> <td style="width: 23.96204%; height: 99px;"> <p><code>batchedPreQueue</code></p> </td> <td style="width: 29.537367%; height: 99px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Definition 3.1</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>spec</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Lemma 3.2</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>isConcreteSpec</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Theorem 3.3</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>noninterference</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Corollary 3.4</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>modularity</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Example 3.5</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Queue.Examples</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>Demo</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Example 3.6</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Queue.Examples</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>QueueReverse</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> </tbody> </table> <p> </p> <p><strong>Download, installation, and sanity-testing</strong></p> <p>1. Install Agda v2.8.0 (<a href="https://agda.readthedocs.io/en/v2.8.0/getting-started/installation.html">instructions</a>).</p> <p>2. Install the Cubical Agda library v0.9 (<a href="https://github.com/agda/cubical/blob/v0.9/INSTALL.md#registering-the-cubical-library">instructions</a>).</p> <p>To test your installation, run the following command from the present directory:</p> <p><code>agda src/index.agda</code></p> <p>or using Emacs or VS Code, open <code>src/index.agda</code> and load the file by via <code>C-c C-l</code> (pressing Ctrl-C immediately followed by Ctrl-L).</p> <p><strong>Evaluation instructions</strong></p> <p>To evaluate a single claim, navigate to the directory containing the file associated with that claim and run agda filename on the command line. Because the validity of each claim is equivalent to Agda being able to typecheck the function with no errors, the expected output is that Agda will finish running with no output.</p> <p>For convenience, a root file <code>src/index.agda</code> imports all files contained in the project, so running <code>agda index.agda</code> in the directory <code>src</code> will effectively evaluate all claims at once. Again, the expected output is that Agda finishes typechecking with no errors or textual outputs. Note that running <code>agda index.agda</code> should not take more than a few minutes.</p> <p><strong>Additional artifact description</strong></p> <p>The file structure included is as follows:</p> <p><code>src</code><br><code>├── Modality</code><br><code>│   ├── Abstract.agda</code><br><code>│   ├── Concrete.agda</code><br><code>│   └── Glue.agda</code><br><code>├── Semantics</code><br><code>│   ├── Abstract.agda</code><br><code>│   └── Concrete.agda</code><br><code>├── Queue</code><br><code>│   ├── Base.agda</code><br><code>│   ├── Examples.agda</code><br><code>│   ├── Glued.agda</code><br><code>│   └── Quotient.agda</code><br><code>├── index.agda</code><br><code>├── Modality.agda</code><br><code>├── Semantics.agda</code><br><code>└── Queue.agda</code></p> <ul> <li><code>index</code> imports all other files, for convenience.</li> <li><code>Modality</code> imports its sub-files, all of which are parameterized by a proposition <code>(ABS : Type) (ABS-isProp : isProp ABS)</code>. <ul> <li><code>Modality.Abstract</code> implements the abstract modality and some relevant lemmas.</li> <li><code>Modality.Concrete</code> implements the concrete modality and some relevant lemmas.</li> <li><code>Modality.Glue</code> implements (a special case of) gluing relative to the ABS proposition and some relevant auxiliary functions and lemmas.</li> </ul> </li> <li><code>Semantics</code> imports its sub-files. <ul> <li><code>Semantics.Abstract</code> instantiates the modalities with the proposition ABS being truth, extracting the abstract aspect.</li> <li><code>Semantics.Concrete</code> instantiates the modalities with the proposition ABS being falsity, extracting the concrete aspect.</li> </ul> </li> <li><code>Queue</code> imports its sub-files, all of which are parameterized by a proposition <code>(ABS : Type) (ABS-isProp : isProp ABS)</code> and a pointed set <code>(E : Type) (e₀ : E) (ESet : isSet E)</code>. <ul> <li><code>Queue.Base</code> defines the pre-queue and queue types, list-based queues, and some associated lemmas.</li> <li><code>Queue.Glued</code> defines batched queues via gluing.</li> <li><code>Queue.Quotient</code> defines batched queues via a phased quotient type.</li> <li><code>Queue.Examples</code> implements some example verifications about queues using noninterference.</li> </ul> </li> </ul> <p><strong>Acknowledgments</strong></p> <p>This formalization builds on prior works, including</p> <ul> <li>the Rocq formalization of Modalities in HoTT by Rijke, Shulman, and Spitters (https://github.com/HoTT/Coq-HoTT/tree/master/theories/Modalities);</li> <li>the Cubical Agda library 1Lab (https://1lab.dev) by the 1Lab Development Team;</li> <li>the Cubical Agda formalization of Modalities in HoTT by Favier (https://agda.monade.li/ErasureOpen); and</li> <li>the Cubical Agda formalization of batched queues as a quotient by Angiuli, Cavallo, Mörtberg, and Zeuner (in <a href="https://github.com/agda/cubical/tree/master/Cubical/Data/Queue">Cubical.Data.Queue</a>).</li> </ul> <p>Additionally, the authors wish to thank Naïm Camille Favier, Amélia Liao, and Tesla Zhang for their invaluable advice pertaining to this project.</p>
format	Recurso digital
id	zenodo_https___doi_org_10_5281_zenodo_17344235
institution	Zenodo
language
publishDate	2025
publisher	Zenodo
record_format	zenodo
spellingShingle	Abstraction Functions as Types Grodin, Harrison Li, Runming Harper, Robert <p><strong>Abstraction Functions as Types</strong></p> <p>This repository contains a Cubical Agda formalization of the queue examples and a corresponding library of phase primitives and lemmas from the paper “Abstraction Functions as Types”.</p> <p><strong>List of claims</strong></p> <table style="width: 79.773157%; height: 14px; border-collapse: collapse; border-spacing: 0px; border-width: 1px; margin-left: 0px; margin-right: auto;"> <tbody> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p><strong>Section</strong></p> <p> </p> </td> <td style="width: 21.593918%; height: 80px;"> <p><strong>Item</strong></p> <p> </p> </td> <td style="width: 15.183867%; height: 80px;"> <p><strong>File</strong></p> <p> </p> </td> <td style="width: 23.96204%; height: 80px;"> <p><strong>Name</strong></p> <p> </p> </td> <td style="width: 29.537367%; height: 80px;"> <p><strong>Notes</strong></p> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Definition 2.1</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>◯</code></p> </td> <td style="width: 29.537367%; height: 80px;"> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Definition 2.2</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Concrete</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>●</code></p> </td> <td style="width: 29.537367%; height: 80px;"> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Lemma 2.3</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>isConcrete</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p>by definition</p> </td> </tr> <tr style="height: 99px;"> <td style="width: 9.604184%; height: 99px;"> <p>§2.1.1</p> </td> <td style="width: 21.593918%; height: 99px;"> <p>Semantics 1</p> </td> <td style="width: 15.183867%; height: 99px;"> <p>Semantics.Abstract</p> </td> <td style="width: 23.96204%; height: 99px;"> <p><code>◯-semantics</code> and <code>●-semantics</code></p> </td> <td style="width: 29.537367%; height: 99px;"> </td> </tr> <tr style="height: 99px;"> <td style="width: 9.604184%; height: 99px;"> <p>§2.1.1</p> </td> <td style="width: 21.593918%; height: 99px;"> <p>Semantics 2</p> </td> <td style="width: 15.183867%; height: 99px;"> <p>Semantics.Concrete</p> </td> <td style="width: 23.96204%; height: 99px;"> <p><code>◯-semantics</code> and <code>●-semantics</code></p> </td> <td style="width: 29.537367%; height: 99px;"> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.1.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Glue</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Glue</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>Glue'</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p>applies modalities, for convenience</p> </td> </tr> <tr style="height: 99px;"> <td style="width: 9.604184%; height: 99px;"> <p>§2.1.2</p> </td> <td style="width: 21.593918%; height: 99px;"> <p>Theorem 2.4</p> </td> <td style="width: 15.183867%; height: 99px;"> <p>Modality.Glue</p> </td> <td style="width: 23.96204%; height: 99px;"> <p><code>glue</code></p> </td> <td style="width: 29.537367%; height: 99px;"> <p>only defining one of the involved maps</p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.2.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>PreQueue</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Queue.Base</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>PreQueue</code></p> </td> <td style="width: 29.537367%; height: 80px;"> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§2.2.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p><em>X</em>, empty, enqueue, dequeue</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Queue.Glued</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>batchedPreQueue</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 99px;"> <td style="width: 9.604184%; height: 99px;"> <p>§2.3.1</p> </td> <td style="width: 21.593918%; height: 99px;"> <p>Batch, empty, enqueue, dequeue</p> </td> <td style="width: 15.183867%; height: 99px;"> <p>Queue.Quotient</p> </td> <td style="width: 23.96204%; height: 99px;"> <p><code>batchedPreQueue</code></p> </td> <td style="width: 29.537367%; height: 99px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.1</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Definition 3.1</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>spec</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Lemma 3.2</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>isConcreteSpec</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Theorem 3.3</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>noninterference</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Corollary 3.4</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Modality.Abstract</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>modularity</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Example 3.5</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Queue.Examples</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>Demo</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> <tr style="height: 80px;"> <td style="width: 9.604184%; height: 80px;"> <p>§3.2</p> </td> <td style="width: 21.593918%; height: 80px;"> <p>Example 3.6</p> </td> <td style="width: 15.183867%; height: 80px;"> <p>Queue.Examples</p> </td> <td style="width: 23.96204%; height: 80px;"> <p><code>QueueReverse</code></p> </td> <td style="width: 29.537367%; height: 80px;"> <p> </p> </td> </tr> </tbody> </table> <p> </p> <p><strong>Download, installation, and sanity-testing</strong></p> <p>1. Install Agda v2.8.0 (<a href="https://agda.readthedocs.io/en/v2.8.0/getting-started/installation.html">instructions</a>).</p> <p>2. Install the Cubical Agda library v0.9 (<a href="https://github.com/agda/cubical/blob/v0.9/INSTALL.md#registering-the-cubical-library">instructions</a>).</p> <p>To test your installation, run the following command from the present directory:</p> <p><code>agda src/index.agda</code></p> <p>or using Emacs or VS Code, open <code>src/index.agda</code> and load the file by via <code>C-c C-l</code> (pressing Ctrl-C immediately followed by Ctrl-L).</p> <p><strong>Evaluation instructions</strong></p> <p>To evaluate a single claim, navigate to the directory containing the file associated with that claim and run agda filename on the command line. Because the validity of each claim is equivalent to Agda being able to typecheck the function with no errors, the expected output is that Agda will finish running with no output.</p> <p>For convenience, a root file <code>src/index.agda</code> imports all files contained in the project, so running <code>agda index.agda</code> in the directory <code>src</code> will effectively evaluate all claims at once. Again, the expected output is that Agda finishes typechecking with no errors or textual outputs. Note that running <code>agda index.agda</code> should not take more than a few minutes.</p> <p><strong>Additional artifact description</strong></p> <p>The file structure included is as follows:</p> <p><code>src</code><br><code>├── Modality</code><br><code>│   ├── Abstract.agda</code><br><code>│   ├── Concrete.agda</code><br><code>│   └── Glue.agda</code><br><code>├── Semantics</code><br><code>│   ├── Abstract.agda</code><br><code>│   └── Concrete.agda</code><br><code>├── Queue</code><br><code>│   ├── Base.agda</code><br><code>│   ├── Examples.agda</code><br><code>│   ├── Glued.agda</code><br><code>│   └── Quotient.agda</code><br><code>├── index.agda</code><br><code>├── Modality.agda</code><br><code>├── Semantics.agda</code><br><code>└── Queue.agda</code></p> <ul> <li><code>index</code> imports all other files, for convenience.</li> <li><code>Modality</code> imports its sub-files, all of which are parameterized by a proposition <code>(ABS : Type) (ABS-isProp : isProp ABS)</code>. <ul> <li><code>Modality.Abstract</code> implements the abstract modality and some relevant lemmas.</li> <li><code>Modality.Concrete</code> implements the concrete modality and some relevant lemmas.</li> <li><code>Modality.Glue</code> implements (a special case of) gluing relative to the ABS proposition and some relevant auxiliary functions and lemmas.</li> </ul> </li> <li><code>Semantics</code> imports its sub-files. <ul> <li><code>Semantics.Abstract</code> instantiates the modalities with the proposition ABS being truth, extracting the abstract aspect.</li> <li><code>Semantics.Concrete</code> instantiates the modalities with the proposition ABS being falsity, extracting the concrete aspect.</li> </ul> </li> <li><code>Queue</code> imports its sub-files, all of which are parameterized by a proposition <code>(ABS : Type) (ABS-isProp : isProp ABS)</code> and a pointed set <code>(E : Type) (e₀ : E) (ESet : isSet E)</code>. <ul> <li><code>Queue.Base</code> defines the pre-queue and queue types, list-based queues, and some associated lemmas.</li> <li><code>Queue.Glued</code> defines batched queues via gluing.</li> <li><code>Queue.Quotient</code> defines batched queues via a phased quotient type.</li> <li><code>Queue.Examples</code> implements some example verifications about queues using noninterference.</li> </ul> </li> </ul> <p><strong>Acknowledgments</strong></p> <p>This formalization builds on prior works, including</p> <ul> <li>the Rocq formalization of Modalities in HoTT by Rijke, Shulman, and Spitters (https://github.com/HoTT/Coq-HoTT/tree/master/theories/Modalities);</li> <li>the Cubical Agda library 1Lab (https://1lab.dev) by the 1Lab Development Team;</li> <li>the Cubical Agda formalization of Modalities in HoTT by Favier (https://agda.monade.li/ErasureOpen); and</li> <li>the Cubical Agda formalization of batched queues as a quotient by Angiuli, Cavallo, Mörtberg, and Zeuner (in <a href="https://github.com/agda/cubical/tree/master/Cubical/Data/Queue">Cubical.Data.Queue</a>).</li> </ul> <p>Additionally, the authors wish to thank Naïm Camille Favier, Amélia Liao, and Tesla Zhang for their invaluable advice pertaining to this project.</p>
title	Abstraction Functions as Types
url	https://doi.org/10.5281/zenodo.17344235