Pith. sign in

REVIEW 4 minor 1 cited by

Bidirectional Elaborators \`a la Carte

T0 review · 0 major / 4 minor · reviewed 2026-07-14 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Elaboration scripts become equational calculations in a monadic DSL, correct by construction and stable under substitution.

desk verdict Clean monadic foundation for correct-by-construction bidirectional elaboration, extracted algebraically from the bi-initial model; solid math, limited scope, ready for referees. read the letter →

arxiv 2607.09564 v2 pith:IXUJ5FU2 submitted 2026-07-10 cs.PL cs.LO

Andrew Slattery , Jonathan Sterling This is my paper · ORCID
classification cs.PLcs.LO MSC 68N1803B3818C50
keywords bidirectionalelaborationMartin-Löftypetheorypartialitymonadpresheafsemanticsnaturalmodelssecond-ordergeneralisedalgebraictheoriescorrect-by-constructionelaboratorsstable
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Proof assistants translate implicit surface code into explicit core terms by elaboration, but that process usually depends on ad-hoc calls to conversion checking and reduction. This paper gives a monadic domain-specific language in which bidirectional surface syntax for Martin-Löf type theory is shallowly embedded, so that translating a surface term into a core term is ordinary equational calculation. The embedding guarantees that only well-typed core terms are produced, that the result is insensitive to judgemental equality of core terms, and that it is stable under substitution; the last property supplies a denotational account of suspended elaboration problems. A concrete algorithm is then extracted, by initiality, from a presheaf model built on the bi-initial natural model of the core theory. A sympathetic reader cares because the framework separates the design of surface languages from the details of normalisation, while still guaranteeing the reliability properties that production elaborators need.

What carries the argument

The partiality relative 2-monad L(X) = (φ : S) × (φ → X) over a dominance of strengthenable levelwise-decidable propositions, equipped with compact-arity lax monoidal structure (the scope combinator) that interprets binders, and with free algebras typ, syn and chk that host the elaboration combinators.

What would settle it

Exhibit a concrete surface term whose equational unfolding inside the monadic DSL either fails to terminate, produces an ill-typed core term, or changes under reordering of independent awaits or under substitution, when evaluated in the bi-initial natural model with the stated dominance.

Watch

Extended reading notes

Core claim

A shallow embedding of bidirectional surface syntax for Martin-Löf type theory into a partiality-monad DSL makes the translation of surface terms into core terms amount to elementary equational calculation; the translation is correct by construction (it cannot produce ill-typed terms) and is automatically stable under judgemental equality and under substitution, yielding a denotational interpretation of suspended elaboration problems. A concrete elaboration algorithm is extracted algebraically from a presheaf model of the DSL built on the bi-initial natural model.

Load-bearing premise

The core theory’s types and terms must be discrete and compact, type-constructor preimages open-subsingleton, and strengthening must hold for the chosen dominance; these rest on external normalisation and injectivity results that the paper cites rather than re-proves.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 4 minor

Summary. The paper introduces a dependently typed monadic DSL, based on a partiality relative 2-monad over a dominance, for the executable specification of correct-by-construction bidirectional elaborators. A bidirectionally typed surface language for Martin-Löf type theory is shallowly embedded so that surface-to-core translation reduces to equational calculation in the metalanguage; the resulting elaborators are well-typed by construction, respect judgemental equality, and are stable under substitution (yielding a denotational account of suspended problems). Combinators for the usual connectives are defined, multilinearity/multistrictness and inequational subject-reduction laws are proved by calculation, and a concrete algorithm is extracted via the universal property of the bi-initial natural model of a SOGAT of elaboration scripts into a presheaf model on the bi-initial model of MLTT, using the dominance of strengthenable levelwise-decidable propositions.

Significance. If the results hold, the work supplies a modular, denotational foundation for bidirectional elaboration that cleanly separates surface-language design from the details of normalisation and conversion. Correctness, stability under substitution, and a denotational reading of suspension follow from the monadic structure rather than from ad-hoc operational arguments; the algebraic extraction via SOGAT initiality is a clean way to obtain an executable algorithm. The equational case study (§4.6), the multilinearity theorem (Theorem 5.1 / Appendix B), and the subject-reduction inequalities (Theorem 5.3) are concrete, checkable contributions that raise the standard for how elaborators can be specified and reasoned about. The framework is reusable for other SOGATs and is therefore of lasting interest to the type-theory and proof-assistant communities.

minor comments (4)
  1. [§1.2.5, §7] The paper repeatedly notes that metavariables, holes, implicit arguments and type classes are left for future work (§1.2.5, §7). A short forward pointer in the introduction to the precise obstacles (e.g. the need for an extra polynomial-monad layer) would help readers calibrate expectations.
  2. [Theorem 6.4] Theorem 6.4 rests on external normalisation and injectivity results that are correctly cited but not re-proved. A one-sentence reminder of which specific lemmas (e.g. Sterling’s injectivity of type constructors, Bocquet’s levelwise decidability) are being invoked would make the dependency fully transparent.
  3. [Figure 1, §6.4] The SOGAT of elaboration scripts (Figure 1) is described as provisional. It would be useful to state explicitly which equations, if any, are currently imposed and which are deliberately omitted so that later extensions remain free.
  4. [Proposition 6.2] A few typographical slips remain (e.g. “Bocqet” for Bocquet in the proof of Proposition 6.2; occasional missing spaces around math). These are easily corrected in production.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: pure algebraic construction of monadic elaborators from dominance + elaborable natural model, with extraction by initiality; external metatheorems are standard background assumptions, not self-referential reductions.

full rationale

The paper defines a partiality relative 2-monad over a dominance, semantic domains typ/syn/chk/hyp, and elaboration combinators (pi, app, lam, idElim, etc.) by direct monadic code that uses discreteness/compactness/open-subsingleton preimages only as hypotheses (Defs. 4.1–4.6). Correctness-by-construction, multilinearity (Thm. 5.1 + App. B equational calculations), and subject-reduction inequalities (Thm. 5.3) follow by unfolding definitions and monad laws inside the metalanguage; nothing is fitted or defined in terms of the result being proved. The concrete algorithm is obtained by interpreting the SOGAT of elaboration scripts (Fig. 1) into the presheaf model on the bi-initial natural model of MLTT and applying the universal property of the bi-initial model of that SOGAT (§6.5–6.6); this is ordinary initiality, not a circular appeal to the elaborator itself. Theorem 6.4 simply records that the bi-initial model satisfies the elaborability hypotheses with respect to the dominance of strengthenable levelwise-decidable propositions; the supporting facts (decidability of judgemental equality, injectivity of type constructors, strengthening) are classical metatheorems of MLTT, cited from the literature (including co-author prior work on normalisation). Those citations supply independent external assumptions; they do not make any equation of the present paper reduce to itself by construction. No fitted parameters, no uniqueness theorem used to forbid alternatives, no ansatz smuggled via self-citation, and no renaming of a known empirical pattern appear. The derivation is therefore self-contained against its stated axioms.

Assumptions & free parameters 0 free parameters · 4 assumptions · 3 invented entities

The paper works entirely inside constructive mathematics relative to an elementary topos with NNO. The only non-standard ingredients are the dominance of strengthenable levelwise-decidable propositions and the elaborability hypotheses on the bi-initial model; both are justified by known metatheorems rather than postulated ad hoc.

assumptions (4)
  • standard math Existence of the bi-initial natural model of Martin-Löf type theory with answer type (Uemura).
    Used as the target of the Yoneda embedding and the source of the extraction homomorphism (Section 6).
  • domain assumption Normalisation and injectivity of type constructors for the bi-initial model (Coquand, Sterling, Bocquet).
    Required to establish discreteness and open-subsingleton preimages that make the judgemental structure elaborable (Theorem 6.4).
  • domain assumption The class of strengthenable levelwise-decidable propositions forms a dominance for which representables are compact.
    Defines the partiality monad L used throughout Sections 3–5; justified by Bocquet’s results and Hofmann–Streicher lifting.
  • domain assumption Strengthening: (∀x:Tm(α).φ)→φ for open φ.
    Needed for multilinearity of binder-forming combinators (Theorem 5.1); follows from normalisation.
invented entities (3)
  • Partiality relative 2-monad L of open partial elements over a dominance independent evidence
    purpose: Provides the computational effect for fallible, suspendable elaboration scripts.
    Standard Rosolini construction specialised to the chosen dominance; not a new physical entity but a new use of an existing categorical tool.
  • Higher-arity lax monoidal structure (scope combinator) at compact arities
    purpose: Interprets binders and hypothetical judgements without explicit contexts.
    Generalises the usual double strength of a commutative monad; the generalisation itself is new to this paper.
  • SOGAT of untyped elaboration scripts (Figure 1)
    purpose: Supplies the algebraic signature whose initial model yields the extraction homomorphism.
    A provisional signature introduced for the extraction theorem; can be extended later.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Bidirectional Elaborators \`a la Carte." pith.science (2026). https://pith.science/paper/IXUJ5FU2

@misc{pith2026260709564,
  author       = {Pith},
  title        = {Pith review of: Bidirectional Elaborators \`a la Carte},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IXUJ5FU2}},
  note         = {Machine review of arXiv:2607.09564}
}
read the original abstract

Surface syntax in proof assistants like Rocq, Lean, Agda, and Idris is highly implicit, lacking many details that are needed for user-written code to denote precisely defined mathematical objects. Elaboration is an algorithm that accounts for these details by translating surface syntax to an explicit enough core syntax. The reliability and predictability of elaboration relies on several critical properties of the core type system, including decidability of judgemental equality and the injectivity of type constructors; these dependencies are witnessed in a concrete system by explicit calls to conversion checking and weak-head reduction subroutines. We introduce a dependently typed monadic domain specific language for the executable specification of correct-by-construction elaboration algorithms that is abstracted from any particular representation of normal forms or algorithm for conversion checking. In particular, we represent a bidirectionally typed surface language for Martin-L\"of type theory by shallow embedding in this DSL so that the translation of surface terms into core terms amounts to elementary equational calculation. This translation is correct by construction in the sense that it cannot produce ill-typed terms, and is automatically stable under judgemental equality of core terms and even under substitution; from the latter property, we obtain a new denotational interpretation of the suspension of elaboration problems. Finally, a concrete elaboration algorithm is extracted by algebraic means from a presheaf model of the DSL built out of the bi-initial natural model of Martin-L\"of type theory.

Figures

Figures reproduced from arXiv: 2607.09564 by the authors.

Figure 1
Figure 1. The second-order generalised algebraic theory of elaboration scripts. [PITH_FULL_IMAGE:figures/full_fig_p024_1.png] view at source ↗

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Setoids in Intensional Type Theory

    cs.LO 2026-07 accept novelty 6.5 of 10 full

    Displayed setoids in IRU give a sound semantics for ETU and a machine-checked proof of ETU consistency inside safe Agda.

Reference graph

Works this paper leans on

51 extracted references · 7 linked inside Pith · cited by 1 Pith paper

  1. [1]

    Michael Abbott, Thorsten Altenkirch, and Neil Ghani. 2005. Containers: Constructing strictly positive types.Theoretical Computer Science342, 1 (2005), 3–27. doi:10.1016/j.tcs.2005.06.002 Applied Semantics: Selected Topics

    doi:10.1016/j.tcs.2005.06.002 2005

  2. [2]

    Danel Ahman and Andrej Bauer. 2026. Sheaves as oracle computations. arXiv:2602.22135 [math.LO] https://arxiv.org/ abs/2602.22135

    arXiv 2026

  3. [3]

    Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. 2015. Monads need not be endofunctors.Logical Methods in Computer Science11, 1 (2015). doi:10.2168/LMCS-11(1:3)2015

    doi:10.2168/lmcs-11(1:3)2015 2015

  4. [4]

    Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. 1995. Categorical reconstruction of a reduction free normalization proof. InCategory Theory and Computer Science, David Pitt, David E. Rydeheard, and Peter Johnstone (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 182–199. doi:10.1007/3-540-60164-3_27

    doi:10.1007/3-540-60164-3_27 1995

  5. [5]

    Nathanael Arkor, Philip Saville, and Andrew Slattery. 2025. Bicategories of algebras for relative pseudomonads. arXiv:2501.12510 [math.CT] https://arxiv.org/abs/2501.12510

    arXiv 2025

  6. [6]

    Robert Atkey. 2015. An Algebraic Approach to Typechecking and Elaboration. https://bentnib.org/posts/2015-04-19- algebraic-approach-typechecking-and-elaboration.html

    2015

  7. [7]

    Steve Awodey. 2018. Natural models of homotopy type theory.Mathematical Structures in Computer Science28, 2 (2018), 241–286. arXiv:1406.3219 [math.CT] doi:10.1017/S0960129516000268

    arXiv doi:10.1017/s0960129516000268 2018

  8. [8]

    Steve Awodey. 2024. On Hofmann–Streicher universes.Mathematical Structures in Computer Science34, 9 (2024), 1–17. doi:10.1017/S0960129524000203 10Or Lean, if only its core tactics were not so tightly coupled to the axioms of classical logic which (naturally) contradict almost any synthetic approach to anything. Bidirectional Elaborators à la Carte 27

    doi:10.1017/s0960129524000203 2024

Show all 51 references
  1. [9]

    Steve Awodey. 2025. Algebraic Type Theory, Part 1: Martin-Löf algebras. arXiv:2505.10761 [math.CT] https: //arxiv.org/abs/2505.10761

    2025 arXiv

  2. [10]

    Rafaël Bocquet. 2026. Relative induction principles for second-order generalized algebraic theories. PhD thesis. https://rafaelbocquet.gitlab.io/pdfs/thesis.pdf

    2026

  3. [11]

    Thierry Coquand. 1996. An algorithm for type-checking dependent types.Science of Computer Programming26, 1 (1996), 167–177. doi:10.1016/0167-6423(95)00021-6

    1996 doi

  4. [12]

    Thierry Coquand. 2019. Canonicity and normalization for dependent type theory.Theoretical Computer Science777 (2019), 184–191. arXiv:1810.09367 [cs.PL] doi:10.1016/j.tcs.2019.01.015 In memory of Maurice Nivat, a founding father of Theoretical Computer Science - Part I

    2019 doi arXiv

  5. [13]

    2013.A Cosmology of Datatypes: Reusability and Dependent Types

    Pierre-Évariste Dagand. 2013.A Cosmology of Datatypes: Reusability and Dependent Types. Ph. D. Dissertation. University of Strathclyde, Glasgow, Scotland

    2013

  6. [14]

    Jana Dunfield and Neel Krishnaswami. 2021. Bidirectional Typing.ACM Comput. Surv.54, 5, Article 98 (May 2021), 38 pages. doi:10.1145/3450952

    2021 doi

  7. [15]

    Peter Dybjer. 1996. Internal type theory. InTypes for Proofs and Programs: International Workshop, TYPES ’95 Torino, Italy, June 5–8, 1995 Selected Papers, Stefano Berardi and Mario Coppo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 120–134

    1996

  8. [16]

    Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson. 2014. The enriched effect calculus: syntax and seman- tics.Journal of Logic and Computation24, 3 (06 2014), 615–654. arXiv:https://academic.oup.com/logcom/article- pdf/24/3/615/2785623/exs025.pdf doi:10.1093/logcom/exs025

    2014 doi

  9. [17]

    Thiago Felicissimo. 2025. Generic Bidirectional Typing for Dependent Type Theories.ACM Trans. Program. Lang. Syst. 47, 1, Article 2 (April 2025), 42 pages. doi:10.1145/3715095

    2025 doi

  10. [18]

    Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. 2016. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures.Selecta Mathematica - New Series, 24 (3), 2018, pp. 2791-2830(2016). doi:10.1007/ s00029-017-0361-3

    2016

  11. [19]

    Marcelo P. Fiore. 2002. Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus. InProceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP ’02). Association for Computing Machinery, Pittsburgh, ...

    2002 doi

  12. [20]

    2025.The Lean Language Reference: The Type System

    Lean FRO. 2025.The Lean Language Reference: The Type System. https://lean-lang.org/doc/reference/latest/The-Type- System/

    2025

  13. [21]

    Nicola Gambino and Joachim Kock. 2013. Polynomial functors and polynomial monads.Mathematical Proceedings of the Cambridge Philosophical Society154, 1 (2013), 153–192. doi:10.1017/S0305004112000394

    2013 doi

  14. [22]

    Daniel Gratzer and Jonathan Sterling. 2020. Syntactic categories for dependent type theory: sketching and adequacy. (2020). arXiv:2012.10783 [cs.LO] Unpublished manuscript

    2020 arXiv

  15. [23]

    Steve Hill. 1996. Combinators for parsing expressions.Journal of Functional Programming6, 3 (1996), 445–464. doi:10.1017/S0956796800001799

    1996 doi

  16. [24]

    1997.Syntax and Semantics of Dependent Types

    Martin Hofmann. 1997.Syntax and Semantics of Dependent Types. Cambridge University Press, 79–130

    1997

  17. [25]

    Martin Hofmann and Thomas Streicher. 1997. Lifting Grothendieck Universes. (1997). https://www2.mathematik.tu- darmstadt.de/~streicher/NOTES/lift.pdf Unpublished note

    1997

  18. [26]

    Graham Hutton and Erik Meijer. 1998. Monadic parsing in Haskell.Journal of Functional Programming8, 4 (1998), 437–444. doi:10.1017/S0956796898003050

    1998 doi

  19. [27]

    J. M. E. Hyland. 1982. The effective topos. InThe L.E.J. Brouwer Centenary Symposium, A. S. Troelstra and D. Van Dalen (Eds.). North Holland Publishing Company, 165–216

    1982

  20. [28]

    S. C. Johnson. 1975. YACC: Yet another compiler-compiler.Computing Science Technical Report32 (1975). https: //cir.nii.ac.jp/crid/1574231874191646464

    1975

  21. [29]

    Johnstone

    Peter T. Johnstone. 1977.Topos Theory. Academic Press

    1977

  22. [30]

    Johnstone

    Peter T. Johnstone. 2002.Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2. Number 43 in Oxford Logical Guides. Oxford Science Publications

    2002

  23. [31]

    Anders Kock. 1972. Strong functors and monoidal monads.Archiv der Mathematik23, 1 (1972), 113–120. doi:10.1007/ BF01304852

    1972

  24. [32]

    2024.PRINCIPLES.md

    András Kovács. 2024.PRINCIPLES.md. https://github.com/AndrasKovacs/2ltt-impl/blob/ f4e13a73c4fb14bbef7f7451974a52ea3f8d6d62/src/PRINCIPLES.md GitHub repository AndrasKovacs/2ltt-impl, commitf4e13a73c4fb14bbef7f7451974a52ea3f8d6d62

    2024

  25. [33]

    2001.Parsec: Direct Style Monadic Parser Combinators for the Real World

    Daan Leijen and Erik Meijer. 2001.Parsec: Direct Style Monadic Parser Combinators for the Real World. Technical Report UU-CS-2001-27. https://www.microsoft.com/en-us/research/publication/parsec-direct-style-monadic-parser- combinators-for-the-real-world/ User Modeling 2007, 11...

    2001

  26. [34]

    2003.Call-by-Push-Value: A Functional/Imperative Synthesis

    Paul Blain Levy. 2003.Call-by-Push-Value: A Functional/Imperative Synthesis. Kluwer, Semantic Structures in Compu- tation, 2

    2003

  27. [35]

    1992.Sheaves in geometry and logic: a first introduction to topos theory

    Saunders Mac Lane and Ieke Moerdijk. 1992.Sheaves in geometry and logic: a first introduction to topos theory. Springer, New York

    1992

  28. [36]

    Per Martin-Löf. 1986. Amendment to Intuitionistic Type Theory. Notes from a lecture given in Göteborg

    1986

  29. [37]

    Conor Mc Bride. 2019. The types who say ‘ni’. Unpublished manuscript

    2019

  30. [38]

    Zanzi Mihejevs and Jules Hedges. 2025. Canonical bidirectional typechecking. arXiv:2512.07511 [cs.PL] https: //arxiv.org/abs/2512.07511

    2025

  31. [39]

    Eugenio Moggi. 1991. Notions of computation and monads. 93, 1 (1991), 55–92. doi:10.1016/0890-5401(91)90052-4 Selections from 1989 IEEE Symposium on Logic in Computer Science

    1991 doi

  32. [40]

    Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, and Steve Awodey. 2026. A Certifying Proof Assistant for Synthetic Mathematics in Lean. InProceedings of the 15th ACM SIGPLAN International Conference on Certified Programs...

    2026 doi

  33. [41]

    Nordström, K

    B. Nordström, K. Petersson, and J. M. Smith. 2001.Martin-Löf’s type theory. Oxford University Press, Inc., USA, 1–32

    2001

  34. [42]

    Pierce and David N

    Benjamin C. Pierce and David N. Turner. 2000. Local type inference.ACM Transactions on Programming Languages and Systems22, 1 (2000), 1–44

    2000

  35. [43]

    François Pottier and Yann Régis-Gianas. 2006. Towards Efficient, Typed LR Parsers.Electronic Notes in Theoretical Computer Science148, 2 (2006), 155–180. doi:10.1016/j.entcs.2005.11.044 Proceedings of the ACM-SIGPLAN Workshop on ML (ML 2005)

    2006 doi

  36. [44]

    1986.Continuity and effectiveness in topoi

    Guiseppe Rosolini. 1986.Continuity and effectiveness in topoi. Ph. D. Dissertation. University of Oxford

    1986

  37. [45]

    Andrew Slattery. 2023. Pseudocommutativity and Lax Idempotency for Relative Pseudomonads. arXiv:2304.14788 [math.CT]

    2023 arXiv

  38. [46]

    2024.Commutativity of Relative Pseudomonads

    Andrew Slattery. 2024.Commutativity of Relative Pseudomonads. Ph. D. Dissertation. University of Leeds. https: //etheses.whiterose.ac.uk/id/eprint/35372/

    2024

  39. [47]

    2021.First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory

    Jonathan Sterling. 2021.First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. Ph. D. Dissertation. Carnegie Mellon University. doi:10.5281/zenodo.6990769 Version 1.1, revised May 2022

    2021 doi

  40. [48]

    2025.Fuss-free universe hierarchies

    Jonathan Sterling. 2025.Fuss-free universe hierarchies. https://www.jonmsterling.com/01HX/ Blog post

    2025

  41. [49]

    Jonathan Sterling. 2025. Toward a Geometry for Syntax. InThe Mathematical and Philosophical Legacy of Alexander Grothendieck, Marco Panza, Daniele C. Struppa, and Jean-Jacques Szczeciniarz (Eds.). Springer Nature Switzerland, Cham, 391–432. doi:10.1007/978-3-031-68934-5_15

    2025 doi

  42. [50]

    Paul Taylor. 2000. Geometric and higher order logic in terms of abstract Stone duality.Theory and Applications of Categories7, 15 (2000), 284–338

    2000

  43. [51]

    2021.Abstract and Concrete Type Theories

    Taichi Uemura. 2021.Abstract and Concrete Type Theories. Ph. D. Dissertation. Universiteit van Amsterdam, Amsterdam. https://www.illc.uva.nl/cms/Research/Publications/Dissertations/DS-2021-09.text.pdf Bidirectional Elaborators à la Carte 29 A The partiality relative 2-monad De...

    2021

Pith tools

Reviewed July 14, 2026 · model on record in the stance chip above.