Focusing and higher-order abstract syntax

DOI10.1145/1328438.1328482MaRDI QIDQ3189855zbMATH OpenOpenAlexFDO

Authors Noam Zeilberger

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.1328482

zbMATH Keywords

focusinghigher-order abstract syntaxpattern matching

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• Reasoning with higher-order abstract syntax in a logical framework
• scientific article; zbMATH DE number 2185713
• scientific article; zbMATH DE number 2185657
• Primitive recursion for higher-order abstract syntax
• Higher-order abstract syntax in Isabelle/HOL

Cited in

(8)

• Focused and Synthetic Nested Sequents
• Structural focalization
• scientific article; zbMATH DE number 1497799 (Why is no real title available?)
• Elaborating dependent (co)pattern matching: no pattern left behind
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Typed Lambda Calculi and Applications
• Positive focusing is directly useful
• Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Focusing and higher-order abstract syntax

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