On the public citation graph

A type and scope safe universe of syntaxes with binding: their semantics and proofs

https://doi.org/10.1145/3236785
0 signed · 70 inferred · view as graph

Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.

Is this your work? Sign in with ORCID and put your name on the claims that are yours.
Claim with ORCID
Reference health. See whether every reference in this work resolves to a known work and none has been retracted — and get a dated CiteStamped badge you can embed.
See reference health

What this work says

Outgoing claims: the papers this work cites, builds on, or argues with.

inferredcites →https://doi.org/10.1007/11541868_4openalex-snapshot
Mechanized Metatheory for the Masses: The PoplMark Challenge
inferredcites →https://doi.org/10.1007/11617990_16openalex-snapshot
Exploring the Regular Tree Types
inferredcites →https://doi.org/10.1007/3-540-48168-0_32openalex-snapshot
Monadic Presentations of Lambda Terms Using Generalized Inductive Types
inferredcites →https://doi.org/10.1007/3-540-48959-2_11openalex-snapshot
A Finite Axiomatization of Inductive-Recursive Definitions
inferredcites →https://doi.org/10.1007/3-540-60164-3_27openalex-snapshot
Categorical reconstruction of a reduction free normalization proof
inferredcites →https://doi.org/10.1007/978-0-387-35672-3_1openalex-snapshot
Generic Programming within Dependently Typed Programming
inferredcites →https://doi.org/10.1007/978-3-319-21401-6_26openalex-snapshot
The Lean Theorem Prover (System Description)
inferredcites →https://doi.org/10.1007/978-3-642-02273-9_11openalex-snapshot
Initial Algebra Semantics for Cyclic Sharing Structures
inferredcites →https://doi.org/10.1007/978-3-642-12032-9_21openalex-snapshot
Monads Need Not Be Endofunctors
inferredcites →https://doi.org/10.1007/978-3-642-28869-2_22openalex-snapshot
GMeta: A Generic Formal Metatheory Framework for First-Order Representations
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_29openalex-snapshot
Automatically Generated Infrastructure for De Bruijn Syntaxes
inferredcites →https://doi.org/10.1007/978-3-662-49498-1_17openalex-snapshot
Needle & Knot: Binder Boilerplate Tied Up
inferredcites →https://doi.org/10.1007/s001650200016openalex-snapshot
A New Approach to Abstract Syntax with Variable Binding
inferredcites →https://doi.org/10.1007/s10817-011-9219-0openalex-snapshot
Strongly Typed Term Representations in Coq
inferredcites →https://doi.org/10.1007/s10817-011-9225-2openalex-snapshot
The Locally Nameless Representation
inferredcites →https://doi.org/10.1016/0167-6423(94)00022-0openalex-snapshot
Substitution: A formal methods case study using monads and transformations
inferredcites →https://doi.org/10.1016/0168-0072(91)90067-vopenalex-snapshot
Kripke-style models for typed lambda calculus
inferredcites →https://doi.org/10.1016/s0049-237x(09)70189-2openalex-snapshot
Constructive Mathematics and Computer Programming
inferredcites →https://doi.org/10.1017/s0956796807006326openalex-snapshot
Applicative programming with effects
inferredcites →https://doi.org/10.1017/s0956796808006758openalex-snapshot
Data types à la carte
inferredcites →https://doi.org/10.1017/s095679681300018xopenalex-snapshot
Idris, a general-purpose dependently typed programming language: Design and implementation
inferredcites →https://doi.org/10.1017/s0956796897002864openalex-snapshot
The Zipper
inferredcites →https://doi.org/10.1017/s0956796899003366openalex-snapshot
de Bruijn notation as a nested datatype
inferredcites →https://doi.org/10.1023/a:1019964114625openalex-snapshot
A Formalised Proof of the Soundness and Completeness of a Simply Typed Lambda-Calculus with Explicit Substitutions
inferredcites →https://doi.org/10.1109/lics.1999.782615openalex-snapshot
Abstract syntax and variable binding
inferredcites →https://doi.org/10.1145/1411203.1411226openalex-snapshot
Parametric higher-order abstract syntax for mechanized semantics
inferredcites →https://doi.org/10.1145/1481861.1481862openalex-snapshot
Dependently typed programming in Agda
inferredcites →https://doi.org/10.1145/1863543.1863547openalex-snapshot
The gentle art of levitation
inferredcites →https://doi.org/10.1145/242224.242477openalex-snapshot
Building domain-specific embedded languages
inferredcites →https://doi.org/10.1145/2429069.2429075openalex-snapshot
Copatterns
inferredcites →https://doi.org/10.1145/2480359.2429075openalex-snapshot
Copatterns
inferredcites →https://doi.org/10.1145/2500365.2500618openalex-snapshot
A nanopass framework for commercial compiler development
inferredcites →https://doi.org/10.1145/2544174.2500618openalex-snapshot
A nanopass framework for commercial compiler development
inferredcites →https://doi.org/10.1145/2976002.2976013openalex-snapshot
Pattern synonyms
inferredcites →https://doi.org/10.1145/3018610.3018613openalex-snapshot
Type-and-scope safe programs and their proofs
inferredcites →https://doi.org/10.1145/3158104openalex-snapshot
Intrinsically-typed definitional interpreters for imperative languages
inferredcites →https://doi.org/10.1145/3167081openalex-snapshot
Triangulating context lemmas
inferredcites →https://doi.org/10.1145/3167098openalex-snapshot
Binder aware recursion over well-scoped de Bruijn syntax
inferredcites →https://doi.org/10.1145/345099.345100openalex-snapshot
Local type inference
inferredcites →https://doi.org/10.4204/eptcs.43.2openalex-snapshot
MiniAgda: Integrating Sized and Dependent Types
inferredcites →https://doi.org/10.48550/arxiv.1804.00119openalex-snapshot
Generic Description of Well-Scoped, Well-Typed Syntaxes
inferredcites →https://doi.org/10.6092/issn.1972-5787/4389openalex-snapshot
Relative Monads Formalised

What points at this work

Incoming claims: where this work appears in other papers’ reference lists and arguments.

inferred← citeshttps://doi.org/10.1007/978-3-030-45231-5_26openalex-snapshot
Semantical Analysis of Contextual Types
inferred← citeshttps://doi.org/10.1007/978-3-030-61467-6_6openalex-snapshot
UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms
inferred← citeshttps://doi.org/10.1007/978-3-030-99253-8_20openalex-snapshot
Variable binding and substitution for (nameless) dummies
inferred← citeshttps://doi.org/10.1007/978-3-031-10769-6_36openalex-snapshot
Rensets and Renaming-Based Recursion for Syntax with Bindings
inferred← citeshttps://doi.org/10.1007/978-3-031-74558-4_2openalex-snapshot
Free Monads, Intrinsic Scoping, and Higher-Order Preunification
inferred← citeshttps://doi.org/10.1007/978-3-031-91118-7_8openalex-snapshot
Artifact Report: an Abstract, Certified Account of Operational Game Semantics
inferred← citeshttps://doi.org/10.1007/978-981-97-8943-6_3openalex-snapshot
Generic Reasoning of the Locally Nameless Representation
inferred← citeshttps://doi.org/10.1007/s10817-019-09522-2openalex-snapshot
A Formalized General Theory of Syntax with Bindings: Extended Version
inferred← citeshttps://doi.org/10.1007/s10817-023-09672-4openalex-snapshot
Rensets and Renaming-Based Recursion for Syntax with Bindings Extended Version
inferred← citeshttps://doi.org/10.1017/s0956796819000170openalex-snapshot
POPLMark reloaded: Mechanizing proofs by logical relations
inferred← citeshttps://doi.org/10.1017/s0956796825100087openalex-snapshot
Towards type-directed compiler calculation
inferred← citeshttps://doi.org/10.1145/3290335openalex-snapshot
Bindings as bounded natural functors
inferred← citeshttps://doi.org/10.1145/3293880.3294101openalex-snapshot
Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions
inferred← citeshttps://doi.org/10.1145/3406088.3409015openalex-snapshot
Stitch: the sound type-indexed type checker (functional pearl)
inferred← citeshttps://doi.org/10.1145/3408972openalex-snapshot
A unified view of modalities in type systems
inferred← citeshttps://doi.org/10.1145/3486609.3487201openalex-snapshot
Extracting the power of dependent types
inferred← citeshttps://doi.org/10.1145/3497775.3503678openalex-snapshot
Implementing a category-theoretic framework for typed abstract syntax
inferred← citeshttps://doi.org/10.1145/3563355openalex-snapshot
Intrinsically-typed definitional interpreters à la carte
inferred← citeshttps://doi.org/10.1145/3689786openalex-snapshot
Type Inference Logics
inferred← citeshttps://doi.org/10.1145/3704893openalex-snapshot
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
inferred← citeshttps://doi.org/10.1145/3747524openalex-snapshot
Correctness Meets Performance: From Agda to Futhark
inferred← citeshttps://doi.org/10.1145/3756907.3756921openalex-snapshot
Formalizing Languages with Binding Operators in Rewriting Logic
inferred← citeshttps://doi.org/10.1145/3763052openalex-snapshot
Pyrosome: Verified Compilation for Modular Metatheory
inferred← citeshttps://doi.org/10.1145/3838790.3838793openalex-snapshot
Effects with Variable Binding
inferred← citeshttps://doi.org/10.22152/programming-journal.org/2021/5/7openalex-snapshot
Programming Metamorphic Algorithms: An Experiment in Type-Driven Algorithm Design
inferred← citeshttps://doi.org/10.4204/eptcs.291.5openalex-snapshot
Value-Dependent Session Design in a Dependently Typed Language
inferred← citeshttps://doi.org/10.46298/lmcs-20(1:18)2024openalex-snapshot
Variable binding and substitution for (nameless) dummies
inferred← citeshttps://doi.org/10.48550/arxiv.2107.11674openalex-snapshot
Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS
Editorial review for independent work. ICSAC — the Institute for Complexity Science and Advanced Computing — runs a structured editorial panel for researchers publishing outside journals, and publishes on CiteStamp rails. Submission is free and goes through ORCID: icsacinstitute.org/submit.