2022/01/19 by Huang, Xu
Computer Science · #03B70 (Primary) 68Q60 (Secondary) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2201.08811
openalex publication_date 2022/01/19 · openalex created_date 2022/05/05 · openalex updated_date 2026/07/28
This article explores a generic framework of well-typed and well-scoped syntaxes, with a signature-axiom approach resembling traditional abstract algebra. The boilerplate code needed in defining operations on syntaxes is identified and abstracted away. Some of the frequent boilerplate proofs are also generalized.