Pith. sign in

REVIEW 3 major objections 4 minor 63 references

Functional programming with lambda-tree syntax

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read MLTS is a new functional language in which binders that occur inside data structures are moved, during evaluation, to binders in the program itself.

desk verdict Genuinely new ML-family design for binder mobility with a working prototype and a precise semantics; the meta-theorems are sketched rather than proved, so treat them as commitments. read the letter →

arxiv 1908.03619 v1 pith:ZSTLENPP submitted 2019-08-09 cs.PL

Ulysse Gérard , Dale Miller , Gabriel Scherer This is my paper · ORCID
classification cs.PL
keywords MLTSlambda-treesyntaxbindermobilitynominalabstractionnablaquantifierfunctionalprogrammingnaturalsemanticshigher-orderpatternunification
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

MLTS is a functional language of the ML family that treats the abstract syntax of terms containing binders as simply typed $\lambda$-terms. Its central design move is binder mobility: a binder that appears inside a data structure is not encoded with names, de Bruijn indices, or a separate binding library; instead, at evaluation time it can move to a binder in the program itself, such as a fresh-nominal construct or a pattern binder. The paper defines evaluation by a natural semantics written as a logical theory in a logic with nominal abstraction and the nabla-quantifier, and states three metatheorems: a closed term's value never contains a free nominal, well-typed evaluation preserves type, and evaluation is deterministic. A prototype interpreter exists, so the intended reading is that this design makes binding-aware programming direct and safe.

What carries the argument

The load-bearing object is the logic G, a logic equipped with fixed points, induction, coinduction, nominal abstraction, and the nabla-quantifier $\nabla$. Nominal abstraction $s \triangleright t$ lets a term built with explicit nominals be re-expressed as a $\lambda$-abstraction over those nominals; it is what makes pattern matching against `nab` binders a logical operation rather than a syntactic special case. The $\nabla$-quantifier, together with the rule $\vdash \nabla X.(E X) \Downarrow V \vdash \mathsf{new}(\lambda X.E X) \Downarrow V$, is exactly the mechanism that prevents a fresh nominal from escaping its scope, since the scope of $\nabla$ sits inside the universal quantification over the value V. The restriction to higher-order pattern unification, where pattern variables are applied only to distinct bound nominals, keeps matching decidable and unitary; and the typing rules use open types and a second arrow $\Rightarrow$ to allow nominals and binding abstractions to appear in data.

What would settle it

Inspect the small-step rules and run the program `new X in X`: the paper predicts the term is stuck, because the rule popping a `new` binder applies only when $X \notin V$. A successful step to a value, or a derivation in logic G proving $\exists V.(\mathsf{new}(\lambda X.X)) \Downarrow V$, would refute the no-escape theorem.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that the $\lambda$-tree syntax approach, already successful in logic programming and theorem proving, can be brought into a functional language by adding two arrow type constructors (the ordinary function arrow $\to$ and the binding arrow $\Rightarrow$), a fresh-nominal construct `new X in ...`, a nominal abstraction operator `X \ body`, an application-of-abstractions operator `@`, and `nab` binders in match rules. Evaluation is specified by natural-semantics rules in the logic G, where the rule for `new` has a premise $\nabla X.(E X) \Downarrow V$; the nabla-quantifier is what guarantees that the fresh nominal X cannot occur free in the value V. The paper claims three theorems: nominals do not escape their scopes, typing is preserved by evaluation, and evaluation is deterministic; these rest on a restriction that every `nab`-bound nominal has a rigid occurrence in the pattern, so pattern matching picks a unique ambient nominal.

Load-bearing premise

The paper's guarantees about evaluation are backed by proofs that are not printed here, promised instead in a future dissertation, and by an online interpreter that is not formally shown to implement the stated semantics.

Editorial extensions

If this is right

  • Programs that manipulate syntax with binders can be written without name generation or de Bruijn bookkeeping; the size, substitution, and $\beta$-normalization examples all follow this pattern.
  • Because bound names are never values, implementations are free to represent binders with de Bruijn indices or other nameless representations, including constant-time binder movement when the binding moves to `new`.
  • The no-escape theorem means `new X in X` is a stuck program, not a value; nominal escape is a dynamic failure the semantics can detect.
  • Type preservation and determinism hold for the core language under the stated pattern restrictions, so a well-typed MLTS program that evaluates does not change type and has a unique result.
  • The `nab` construct transfers generic-judgment reasoning into functional pattern matching, letting a clause match an anonymous nominal.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the deferred proofs in the thesis check out, the same logic-G presentation could be reused as a template for giving natural semantics to other languages with binder mobility.
  • A natural next experiment is to prove an equivalence between the big-step natural semantics and the small-step operational semantics of the paper; that would make the co-evolved online interpreter a verified implementation of the specification.
  • The static checks sketched in the paper for skipping escape checks could be benchmarked: type-directed elimination of escape checks may recover the constant-time binder moves the authors describe for common cases.
  • The paper's closing discussion suggests that a linear-logic variant of the same semantics could host references and other effects, which would test whether binder mobility extends beyond pure functional programs.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

Summary. The paper introduces MLTS, a functional language extending core ML with lambda-tree syntax. The central design claims are that (i) binders in data structures can move to program-level binders via new constructs (new X in, backslash, @, nab), (ii) evaluation can be specified as a natural semantics in logic G using nominal abstraction and the nabla-quantifier, and (iii) the language satisfies three meta-theoretic properties: nominals do not escape (Theorem 4.1), type preservation (Theorem 4.2), and determinacy of evaluation (Theorem 4.3). The paper also presents a typing discipline, restrictions on patterns (unique occurrence, higher-order pattern variables under the Lλ restriction, and rigid occurrence of nab-bound nominals), a small-step operational semantics, and a prototype implementation in λProlog with an online interface.

Significance. MLTS is a well-motivated design that brings the lambda-tree syntax approach from logic programming (λProlog, Abella) into a functional language and demonstrates it on a range of convincing examples (size, substitution, β-normal form, De Bruijn conversion, higher-order maptm). The novel combination of nominal abstraction and nabla in a natural semantics is a promising way to give binding-aware languages a declarative specification. The paper also honestly discusses design trade-offs (β0 versus β, dynamic escape failures versus static disciplines). If the three theorems are fully proved, they would establish for a nontrivial language that binder mobility can be given a deterministic, type-preserving operational semantics with no nominal escape, a result of interest to both the programming-languages and logical-frameworks communities. The online prototype is a valuable artifact for replicating the examples. However, the formal support for these theorems is currently deferred, and the correspondence between the two semantic presentations is asserted rather than proved; these gaps must be addressed before the formal claims can be accepted.

major comments (3)
  1. [§4.4] Theorems 4.1–4.3 are stated with only proof sketches; Section 4.4 says "Detailed proofs of these theorems can be found in the forthcoming Ph.D. dissertation of the first author [19]." Since these theorems are the central formal contribution, the submitted manuscript must contain the complete proofs or a detailed appendix. In particular, the proof of Theorem 4.3 needs to spell out the induction on derivations in Figure 7, including how the negative premise ¬(∃u.clause T Rule u) in the second match rule is handled, and how the rigid-path machinery of §4.2.3, together with the side conditions Y ∉ R X and Y ∉ σ in Figure 13, ensures the unique determination of nab-bound nominals. The current "usual outline" is not sufficient for a refereed formal claim.
  2. [§4.3] Section 4.3 asserts that the small-step semantics is equivalent to the natural semantics of Figure 7, and the paragraph on correspondence says "holds if and only if" for the matching judgment, but no proof of this equivalence is given. This matters because the λProlog implementation is described as co-evolved with the small-step semantics: "the former guiding the latter, with the bugs found playing with the latter informing changes to the former." Without a proof, or at least a precise statement with a proof sketch, the implementation cannot serve as independent evidence for the formal natural semantics, and the paper's claim that MLTS has a formally defined deterministic semantics rests on an unverified correspondence.
  3. [§3.4] The natural semantics specification is only meaningful relative to the logic G, but G is not defined in the paper; the reader is referred to [16,18] for the sequent calculus, cut-elimination, and nominal abstraction algorithms. Since the inference rules of Figure 7 are stated as "notations for formulas in G," a self-contained submission should at least specify the fragment of G used (nabla-quantification, nominal abstraction, and the clause judgment) or state precisely which background theory is being assumed. Without this, the claim that the natural semantics is a formal definition is hard to verify. This issue is local to the presentation of the semantics and could be fixed by an appendix.
minor comments (4)
  1. [§6] Section 6 lists as future work "a first step would be to first design a small-step (SOS) semantics equivalent of our natural semantics," but Section 4.3 already presents a small-step semantics and asserts its equivalence. Either remove this item or explain what additional aspect of the small-step semantics remains to be designed.
  2. [Figure 13] In Figure 13, the rule for matching against nab uses the notation "V with R Y↝ σ,N" and the premise "∇X.∃π,Y. ... Y ∈π R X ... Y ∈π V ..."; the scoping of Y in the premise is not explained. A sentence clarifying the side conditions and the status of Y would help the reader verify the rule.
  3. [Figure 9] The typing rule for pattern @-expressions requires that X1,...,Xn are distinct nominals bound within the scope of the pattern binding on r, but the rule as displayed in Figure 9 does not carry a side condition enforcing distinctness; the prose in §4.2.2 supplies this, but annotating the rule directly would be clearer.
  4. [§4.3] The paper states that, due to space restrictions, it will not give a fully detailed explanation of the small-step semantics, leaving the figures to "speak for themselves." Given that the small-step semantics is one of the two formal presentations of the language, a few more paragraphs of explanation in a revised version would substantially improve accessibility.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; MLTS's metatheorems are new claims about a new language, and the cited prior logic work is background infrastructure rather than the derived conclusion.

full rationale

The paper's central claims are design-level results about a new language, MLTS: a natural-semantics evaluation specification in the logic G, type preservation, determinacy, and non-escape of nominals. The heavy reliance on the authors' own prior work (G, nominal abstraction, the nabla-quantifier, higher-order pattern unification, raising) is real but not circular: those results are imported as background mathematical infrastructure, and the paper's theorems concern the newly defined language built on that infrastructure. Theorem 4.1 ('nominals do not escape') is indeed immediate from the form of the new-rule in Figure 7, but that is a property of the proposed definition, not a prediction derived from an input that already contains it; the proof is a routine induction on derivations in G. Theorems 4.2 and 4.3 are substantive meta-theoretic statements whose proofs are not included here; Section 4.4 explicitly says 'Detailed proofs of these theorems can be found in the forthcoming Ph.D. dissertation of the first author [19].' That is a verification/completeness gap, not circularity. Similarly, Section 4.3 asserts an iff correspondence between the natural and small-step semantics without proof and notes the implementation was co-evolved with the small-step semantics; again, this is an evidential weakness, not a reduction of the conclusion to the premises. No equation or definition in the paper was found in which a claimed prediction is identical by construction to a fitted input or in which a self-citation is the sole load-bearing justification for the target result.

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

The central claim is a language design, so there are no fitted numeric parameters. It rests on the background logic G, on known results about higher-order pattern unification, and on the assumption that the prototype matches the semantics. The main invented entity is the language itself, which has independent evidence through its implementation and examples.

assumptions (4)
  • domain assumption The logic G (with nabla-quantifier, nominal abstraction, fixed points, induction, coinduction) is a consistent and adequate logical foundation for specifying natural semantics.
    Section 3.3-3.4: the natural semantics is defined as formulas in G, relying on cut-elimination for G proved in Gacek 2009 and Gacek et al. 2011 (self-cited).
  • standard math Higher-order pattern unification (L lambda unification) is decidable and unitary, and matching restricts to beta0-conversion, as per Miller 1991.
    Section 4.2.2 invokes these results to justify the restrictions on pattern variables. This is prior published mathematical work, not proved in the paper.
  • domain assumption Nominals are represented as distinct constants in a higher-order abstract syntax context, and alpha-conversion is always available; equality includes alpha-beta-eta-conversion.
    Section 3.1 and the abstract syntax description. This is a design tenet of lambda-tree syntax, not proven.
  • domain assumption The lambdaProlog implementation and the natural semantics are behaviorally aligned.
    Section 4.3 and Section 2.4: the small-step and big-step semantics were co-evolved with the lambdaProlog interpreter, but no formal equivalence proof is given.
invented entities (2)
  • MLTS language and its constructs (new X in, backslash abstraction, @, nab in patterns) independent evidence
    purpose: To enable binder mobility: binders in data structures move to program-level binders, and nominals never escape their scope.
    The paper provides an online interpreter (TryMLTS) and many runnable examples; the semantics and typing rules give a falsifiable specification against which the interpreter can be tested.
  • Nominal constants independent evidence
    purpose: Represent bindable names that behave like constructors; used in new, backslash, and nab constructs.
    Implemented in the prototype; the theorem that nominals do not escape is a falsifiable property.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Functional programming with lambda-tree syntax." pith.science (2026). https://pith.science/paper/ZSTLENPP

@misc{pith2026190803619,
  author       = {Pith},
  title        = {Pith review of: Functional programming with lambda-tree syntax},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ZSTLENPP}},
  note         = {Machine review of arXiv:1908.03619}
}
read the original abstract

We present the design of a new functional programming language, MLTS, that uses the lambda-tree syntax approach to encoding bindings appearing within data structures. In this approach, bindings never become free nor escape their scope: instead, binders in data structures are permitted to move to binders within programs. The design of MLTS includes additional sites within programs that directly support this movement of bindings. In order to formally define the language's operational semantics, we present an abstract syntax for MLTS and a natural semantics for its evaluation. We shall view such natural semantics as a logical theory within a rich logic that includes both *nominal abstraction* and the *nabla-quantifier*: as a result, the natural semantics specification of MLTS can be given a succinct and elegant presentation. We present a typing discipline that naturally extends the typing of core ML programs and we illustrate the features of MLTS by presenting several examples. An on-line interpreter for MLTS is briefly described.

Figures

Figures reproduced from arXiv: 1908.03619 by the authors.

Figure 1
Figure 1. A program for computing the size of a λ-term. let subst t u = new X in let rec aux t = match t with | X -> u | nab Y in Y -> Y | App (u , v ) -> App ( aux u , aux v ) | Abs r -> Abs ( Y\ aux ( r @ Y ) ) in aux (t @ X ) ;; let rec beta t = match t with | nab X in X -> X | Abs r -> Abs ( Y\ beta ( r @ Y ) ) | App (m , n) -> let m = beta m in let n = beta n in begin match m with | Abs r -> beta ( subst r n ) | _ -> App… view at source ↗
Figure 3
Figure 3. Three implementations for determining if an ab [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 2
Figure 2. The function that computes the substitution [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figures from the paper (9 more)
Figure 5
Figure 5. Figure 5: De Bruijn’s style syntax and its conversions with [PITH_FULL_IMAGE:figures/full_fig_p004_5.png]
Figure 6
Figure 6. Figure 6: Various computations on untyped λ-terms using higher-order programs. Note that there are several occur￾rences of (r X) above that should not be written as (r @ X). functions nth and index take a list of nominals as their second ar￾gument: nth takes also an integer n an…
Figure 7
Figure 7. Figure 7: A natural semantics specification of evaluation. [PITH_FULL_IMAGE:figures/full_fig_p007_7.png]
Figure 8
Figure 8. Figure 8: The abstract syntax of the size program. list of clauses. Clauses are built from the infix operator ==>, tak￾ing a pattern on the left and a term on the right, and from quanti￾fiers all, to introduce universally-quantified variables (implicit in MLTS programs), and nab…
Figure 9
Figure 9. Figure 9: Typing rules based on the concrete syntax for the ne [PITH_FULL_IMAGE:figures/full_fig_p009_9.png]
Figure 11
Figure 11. Figure 11: Small step reduction: core fragment namely, using the terms X\Y\X and X\Y\Y. This breaks the deter￾minacy property – Theorem 4.3. In the second example, the nom￾inal X is completely unconstrained by the pattern. If this program was allowed, our natural semantics dicta…
Figure 10
Figure 10. Figure 10: Code that does not satisfy the restriction on oc [PITH_FULL_IMAGE:figures/full_fig_p010_10.png]
Figure 13
Figure 13. Figure 13: Small step reduction: pattern-matching not a value, but any value V X can be eta-expanded to the (non￾value) form (arobase (backslash λX.V X) X), so we look for the sub-value at path π in (backslash λX.V X). Operational semantics of pattern matching. The treatment of …
Figure 12
Figure 12. Figure 12: Rigid paths in values and patterns at this point of the program execution. In addition to the standard rule allowing reduction under context, we have an extra contex￾tual rule to allow popping a new binder off the context: when the term inside that binder has been ful…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

63 extracted references · 49 canonical work pages

  1. [19]

    Ulysse Gérard. 2019. Computing with relations, functions, and bindings . Ph.D. Dissertation. University of Paris Saclay. http://www.lix.polytechnique.fr/Labo/Dale.Miller/gerard19phd.pdf

    work page 2019

  2. [1]

    Mason, and Robert Poll ack

    Arnon Avron, Furio Honsell, Ian A. Mason, and Robert Poll ack. 1992. Using Typed Lambda Calculus to Implement Formal Systems on a Machi ne. Journal of Automated Reasoning 9 (1992), 309–354. https://doi.org/10.1007/BF00245294

    work page doi:10.1007/bf00245294 1992

  3. [2]

    Aydemir, Aaron Bohannon, Matthew Fairbairn, J

    Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Fos- ter, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytinioti s, Geoffrey Wash- burn, Stephanie Weirich, and Steve Zdancewic. 2005. Mechan ized Metathe- ory for the Masses: The POPLmark Challenge. In Theorem Proving in Higher Order Logics: 18th International Conference (LNCS) . Springer, 50–6...

    doi:10.1007/11541868_4 2005

  4. [3]

    David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Mil ler, Gopalan Na- dathur, Alwen Tiu, and Yuting Wang. 2014. Abella: A System fo r Reasoning about Relational Specifications. Journal of Formalized Reasoning 7, 2 (2014), 1–

    work page 2014

  5. [4]

    Arthur Charguéraud. 2011. The Locally Nameless Represe ntation. Journal of Au- tomated Reasoning (May 2011), 1–46. https://doi.org/10.1007/s10817-011-9225-2

    doi:10.1007/s10817-011-9225-2 2011

  6. [5]

    James Cheney and Christian Urban. 2004. Alpha-Prolog: A Logic Programming Language with Names, Binding, and Alpha-Equivalence. In Logic Programming, 20th International Conference (LNCS), Bart Demoen and Vladimir Lifschitz (Eds.), Vol. 3132. Springer, 269–283. https://doi.org/10.1007/978-3-540-27775-0_19

    work page doi:10.1007/978-3-540-27775-0_19 2004

  7. [6]

    Anthony S. K. Cheng, Peter J. Robinson, and John Staples. 1991. Higher Level Meta Programming in Qu-Prolog 3: 0. In Logic Programming, Proceedings of the Eigth International Conference, Paris, France, June 24-28, 1991, Koichi Furukawa (Ed.). MIT Press, 285–298

    work page 1991

  8. [7]

    Jawahar Chirimar. 1995. Proof Theoretic Approach to Specifica- tion Languages . Ph.D. Dissertation. University of Pennsylvania. http://www.lix.polytechnique.fr/Labo/Dale.Miller/chirimar/phd.ps

    work page 1995

Show all 63 references
  1. [8]

    Adam Chlipala. 2008. Parametric higher-order abstract syntax for mecha- nized semantics. In Proceeding of the 13th ACM SIGPLAN international con- ference on Functional programming, ICFP 2008, Victoria, BC , Canada, Sep- tember 20-28, 2008 , James Hook and Peter Thiemann (Eds.)...

    2008

  2. [9]

    Alonzo Church. 1940. A Formulation of the Simple Theory o f Types. J. of Sym- bolic Logic 5 (1940), 56–68. https://doi.org/10.2307/2266170

    1940 doi

  3. [10]

    Nicolaas Govert de Bruijn. 1972. Lambda Calculus Notat ion with Nameless Dummies, a Tool for Automatic Formula Manipulation, with an Application to the Church-Rosser Theorem. Indagationes Mathematicae 34, 5 (1972), 381–392. https://doi.org/10.1016/1385-7258(72)90034-0

    1972 doi

  4. [11]

    Joëlle Despeyroux, Amy Felty, and Andre Hirschowitz. 1 995. Higher-order ab- stract syntax in Coq. In Second International Conference on Typed Lambda Calculi and Applications. 124–138. https://doi.org/10.1007/BFb0014049

    doi

  5. [12]

    Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Co en, and Enrico Tassi

  6. [13]

    Felty, Alberto Momigliano, and Brigitte Pientka

    Amy P. Felty, Alberto Momigliano, and Brigitte Pientka . 2015. The Next 700 Challenge Problems for Reasoning with Higher-Order Abstra ct Syntax Repre- sentations: Part 2–A Survey. J. of Automated Reasoning 55, 4 (2015), 307–372. https://doi.org/10.1007/s10817-015-9327-3

    2015 doi

  7. [14]

    Francisco Ferreira and Brigitte Pientka. 2017. Progra ms Using Syntax with First- Class Binders. In Proceedings of the 26th European Symposium on Programming, ESOP 2017, Uppsala, Sweden (Lecture Notes in Computer Science), Hongseok Yang (Ed.), Vol. 10201. Springer, 504–529

    2017

  8. [15]

    M. J. Gabbay and A. M. Pitts. 1999. A new approach to abstr act syntax involving binders. In 14th Symp. on Logic in Computer Science . IEEE Computer Society Press, 214–224

    1999

  9. [16]

    Andrew Gacek. 2009. A Framework for Specifying, Prototyping, and Reasoning about Computational Systems . Ph.D. Dissertation. University of Minnesota

    2009

  10. [17]

    Andrew Gacek, Dale Miller, and Gopalan Nadathur. 2008. Combining generic judgments with recursive definitions. In 23th Symp. on Logic in Computer Science , F. Pfenning (Ed.). IEEE Computer Society Press, 33–44. https://doi.org/10.1109/LICS.2008.33

    2008 doi

  11. [18]

    Andrew Gacek, Dale Miller, and Gopalan Nadathur. 2011. Nomi- nal abstraction. Information and Computation 209, 1 (2011), 48–73. https://doi.org/10.1016/j.ic.2010.09.004

    2011 doi

  12. [20]

    Ulysse Gérard, Dale Miller, and Gabriel Scherer. 2018. Try MLTS Online. https://trymlts.github.io/

    2018

  13. [21]

    A. Gordon. 1994. A Mechanisation of Name-Carrying Synt ax up to Alpha- Conversion. In International Workshop on Higher Order Logic Theorem Provin g and its Applications (Lecture Notes in Computer Science) , Vol. 780. 414–426

    1994

  14. [22]

    Gordon, Arthur J

    Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth. 1979. Edin- burgh LCF: A Mechanised Logic of Computation . LNCS, Vol. 78. Springer. PPDP ’19, October 7–9, 2019, Porto, Portugal Ulysse Gérard, Dale Miller, and Gabriel Scherer

    1979

  15. [23]

    Michael J. C. Gordon. 1991. Introduction to the HOL Syst em. In Proceedings of the International Workshop on the HOL Theorem Proving System and its Applications, Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. W indley (Eds.). IEEE Computer Society, 2–3

    1991

  16. [24]

    Robert Harper, Furio Honsell, and Gordon Plotkin. 1993 . A Framework for Defin- ing Logics. J. ACM 40, 1 (1993), 143–184

    1993

  17. [25]

    John Harrison. 2009. HOL Light: an overview. In International Conference on Theorem Proving in Higher Order Logics . Springer, 60–66

    2009

  18. [26]

    Gérard Huet. 1975. A Unification Algorithm for Typed λ-Calculus. Theoretical Computer Science 1 (1975), 27–57. https://doi.org/10.1016/0304-3975(75)90011-0

    1975 doi

  19. [27]

    Js_of_ocaml

    js-of-ocaml 2018. Js_of_ocaml. http://ocsigen.org/js_of_ocaml/

    2018

  20. [28]

    Gilles Kahn. 1987. Natural Semantics. In Proceedings of the Symposium on Theo- retical Aspects of Computer Science (LNCS) , Franz-Josef Brandenburg, Guy Vidal- Naquet, and Martin Wirsing (Eds.), Vol. 247. Springer, 22–3 9

    1987

  21. [29]

    Licata and Robert Harper

    Daniel R. Licata and Robert Harper. 2009. A Universe of B inding and Com- putation. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP ’09) . ACM, New York, NY, USA, 123–134. https://doi.org/10.1145/1596550.1596571

    2009

  22. [30]

    Conor McBride and James McKinna. 2004. Functional pear l: I am not a num- ber - I am a free variable. In Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Snowbird, UT, USA, September 22-22, 2004, Henrik Nilsson (Ed.). ACM, 1–9. http://doi.acm.org/10.1145/10174...

    2004

  23. [31]

    Dale Miller. 1990. An Extension to ML to Handle Bound Var i- ables in Data Structures: Preliminary Report. In Proceedings of the Logical Frameworks BRA Workshop . Antibes, France, 323–335. http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mll.pdf Available as UPenn CIS t...

    1990

  24. [32]

    Dale Miller. 1991. A Logic Programming Language with La mbda-Abstraction, Function Variables, and Simple Unification. J. of Logic and Computation 1, 4 (1991), 497–536. https://doi.org/10.1093/logcom/1.4.497

    1991 doi

  25. [33]

    Dale Miller. 1992. Unification under a mixed prefix. Journal of Symbolic Compu- tation 14, 4 (1992), 321–358. https://doi.org/10.1016/0747-7171(92)90011-R

    1992 doi

  26. [34]

    Dale Miller. 1996. Forum: A Multiple-Conclusion Speci fication Logic. Theoretical Computer Science 165, 1 (Sept. 1996), 201–232. https://doi.org/10.1016/0304-3975(96)00045-X

    1996 doi

  27. [35]

    Dale Miller. 2004. Bindings, mobility of bindings, and the ∇-quantifier. In 18th International Conference on Computer Science Logic (C SL) 2004 (LNCS), Jerzy Marcinkowski and Andrzej Tarlecki (Eds.), Vol. 3210 . 24. https://doi.org/10.1007/978-3-540-30124-0_4

    2004 doi

  28. [36]

    Dale Miller. 2018. Mechanized Metatheory Revisited. Journal of Automated Reasoning (04 Oct. 2018). https://doi.org/10.1007/s10817-018-9483-3

    2018 doi

  29. [37]

    Dale Miller and Gopalan Nadathur. 2012. Programming with Higher-Order Logic. Cambridge University Press. https://doi.org/10.1017/CBO9781139021326

    2012 doi

  30. [38]

    Dale Miller and Catuscia Palamidessi. 1999. Foundatio nal Aspects of Syntax. Comput. Surveys 31 (Sept. 1999)

    1999

  31. [39]

    Dale Miller and Alwen Tiu. 2005. A proof theory for gener ic judg- ments. ACM Trans. on Computational Logic 6, 4 (Oct. 2005), 749–783. https://doi.org/10.1145/1094622.1094628

    2005

  32. [40]

    Gopalan Nadathur and Dale Miller. 1988. An Overview of λProlog. In Fifth International Logic Programming Conference . MIT Press, Seattle, 810–827. http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/iclp88.pdf

    1988

  33. [41]

    Tobias Nipkow. 1993. Functional Unification of Higher- Order Patterns. In 8th Symp. on Logic in Computer Science , M. Vardi (Ed.). IEEE, 64–74

    1993

  34. [42]

    OCaml. 2018. http://ocaml.org/

    2018

  35. [43]

    Lawrence C. Paulson. 1989. The Foundation of a Generic T heorem Prover. Jour- nal of Automated Reasoning 5 (Sept. 1989), 363–397

    1989

  36. [44]

    Lawrence C. Paulson. 1994. Isabelle: A Generic Theorem Prover . Number 828 in LNCS. Springer Verlag

    1994

  37. [45]

    Frank Pfenning and Conal Elliott. 1988. Higher-Order A bstract Syntax. In Pro- ceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, 199–208

    1988

  38. [46]

    Frank Pfenning and Carsten Schürmann. 1999. System Des cription: Twelf — A Meta-Logical Framework for Deductive Systems. In 16th Conf. on Auto- mated Deduction (CADE) (LNAI) , H. Ganzinger (Ed.). Springer, Trento, 202–206. https://doi.org/10.1007/3-540-48660-7_14

    1999 doi

  39. [47]

    Brigitte Pientka and Joshua Dunfield. 2010. Beluga: A Fr amework for Program- ming and Reasoning with Deductive Systems (System Description). In Fifth Inter- national Joint Conference on Automated Reasoning (LNCS), J. Giesl and R. Hähnle (Eds.). 15–21

    2010

  40. [48]

    Andrew M. Pitts. 2003. Nominal Logic, A First Order Theo ry of Names and Binding. Information and Computation 186, 2 (2003), 165–193

    2003

  41. [49]

    A. M. Pitts and M. J. Gabbay. 2000. A Metalanguage for Pro gramming with Bound Names Modulo Renaming. In Mathematics of Program Construction. 5th International Conference, MPC2000, Ponte de Lima, Portugal, J uly 2000. Proceed- ings (LNCS) , R. Backhouse and J. N. Oliveira (Eds...

    2000

  42. [50]

    Adam Poswolsky and Carsten Schürmann. 2008. Practical programming with higher-order encodings and dependent types. In Proceedings of the European Symposium on Programming (ESOP 2008)

    2008

  43. [51]

    Adam Poswolsky and Carsten Schürmann. 2008. System Des cription: Delphin - A Functional Programming Language for Deductive Systems, In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), A. Abel and C. Urban (Eds.). Electr. Notes ...

    2008

  44. [52]

    François Pottier. 2006. An Overview of C α ml. In Proceedings of the ACM- SIGPLAN Workshop on ML (ML 2005) (Electr. Notes Theor. Comput . Sci.), Vol. 148. 27–52. https://doi.org/10.1016/j.entcs.2005.11.039

    2006 doi

  45. [53]

    François Pottier. 2007. Static name control for FreshM L. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007) . IEEE, 356–365

    2007

  46. [54]

    Xiaochu Qi, Andrew Gacek, Steven Holte, Gopalan Nadath ur, and Zach Snow. 2015. The Teyjus System – Version 2. http://teyjus.cs.umn.edu/ http://teyjus.cs.umn.edu/

    2015

  47. [55]

    Davide Sangiorgi. 1996. π -calculus, internal mobility and agent-passing calculi. Theoretical Computer Science 167, 2 (1996), 235–274

    1996

  48. [56]

    Carsten Schürmann, Adam Poswolsky, and Jeffrey Sarnat. 2005. The nabla- calculus. Functional Programming with Higher-order Encodings. In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA’05). https://doi.org/10.1007/11417170_25

    2005 doi

  49. [57]

    Helmut Schwichtenberg. 2006. Minlog. In The Seventeen Provers of the World (LNCS) , Freek Wiedijk (Ed.), Vol. 3600. Springer, 151–157. https://doi.org/10.1007/11542384_19

    2006 doi

  50. [58]

    Dana Scott. 1970. Outline of a Mathematical Theory of Co mputation. In Proceed- ings, Fourth Annual Princeton Conference on Information Sci ences and Systems . Princeton University, 169–176. Also, Programming Researc h Group Technical Monograph PRG–2, Oxford University

    1970

  51. [59]

    M. R. Shinwell, A. M. Pitts, and M. J. Gabbay. 2003. Fresh ML: Programming with Binders Made Simple. In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden . ACM Press, 263–274

    2003

  52. [60]

    Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, and Gopa lan Nadathur

  53. [89]

    https://doi.org/10.6092/issn.1972-5787/4650

    1972 doi

  54. [2013]

    In Proceed- ings of the 15th International Symposium on Princples and Prac tice of Declar- ative Programming (PPDP) , Tom Schrijvers (Ed.)

    Reasoning about Higher-Order Relational Specificati ons. In Proceed- ings of the 15th International Symposium on Princples and Prac tice of Declar- ative Programming (PPDP) , Tom Schrijvers (Ed.). Madrid, Spain, 157–168. https://doi.org/10.1145/2505879.2505889

  55. [2015]

    ELPI: Fast, Embeddable, λProlog Interpreter. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th Internationa l Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings (LNCS) , Martin Davis, Ans- gar Fehnker, Annabelle McIver, and Andrei Voro...

    2015 doi

Pith tools

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