A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
From MaRDI portal
Publication:3189856
DOI10.1145/1328438.1328483zbMath1295.68068OpenAlexW2039769798MaRDI QIDQ3189856
Publication date: 12 September 2014
Published in: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1328438.1328483
Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)
Related Items
The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, Inductive Beluga: Programming Proofs, A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types, A two-level logic approach to reasoning about computations, Unnamed Item, Normalization by evaluation for modal dependent type theory, POPLMark reloaded: Mechanizing proofs by logical relations, Semantical analysis of contextual types, Mtac: A monad for typed tactic programming in Coq, The calculus of dependent lambda eliminations, Programs Using Syntax with First-Class Binders, LINCX: A Linear Logical Framework with First-Class Contexts, Structural recursion with locally scoped names, 2-Dimensional Directed Type Theory, Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), Programming Inductive Proofs, On the Expressivity of Minimal Generic Quantification, A Simple Nominal Type Theory, Explicit Contexts in LF (Extended Abstract), Case Analysis of Higher-Order Data, On the Role of Names in Reasoning about λ-tree Syntax Specifications, Unnamed Item, Harpoon: mechanizing metatheory interactively, A case study in programming coinductive proofs: Howe’s method
