Programming with binders and indexed data-types

DOI10.1145/2103656.2103705MaRDI QIDQ2942890zbMATH OpenOpenAlexFDO

Authors Andrew Cave, Brigitte Pientka

Publication date 11 September 2015

Published in Proceedings of the 39th 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/2103656.2103705

zbMATH Keywords

dependent typeshigher-order abstract syntaxlogical frameworksrecursive types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• FreshML: programming with binders made simple
• A universe of binding and computation
• Programming inductive proofs. A new approach based on contextual types
• Binders unbound
• Refining inductive types

Cited in

(15)

• Programs using syntax with first-class binders
• \textsc{Lincx}: a linear logical framework with first-class contexts
• Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming
• Encoding types in ML-like languages
• A universe of binding and computation
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• A case study in programming coinductive proofs: Howe's method
• Inductive beluga: programming proofs
• Mtac: a monad for typed tactic programming in Coq
• A modal analysis of metaprogramming, revisited (invited talk)
• Index-stratified types
• POPLMark reloaded: mechanizing proofs by logical relations
• Harpoon: mechanizing metatheory interactively
• A case study on logical relations using contextual types
• An open challenge problem repository for systems supporting binders

Describes a project that uses

Uses Software

• VeriML
• ML
• Coq

This page was built for publication: Programming with binders and indexed data-types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2942890)