How to prove decidability of equational theories with second-order computation analyser SOL

DOI10.1017/S0956796819000157zbMath1442.68027OpenAlexW2996342526MaRDI QIDQ5110922

Makoto Hamana

Publication date: 26 May 2020

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796819000157

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Decidability of theories and sets of sentences (03B25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Monoidal categories, symmetric monoidal categories (18M05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding ⋮ Unnamed Item ⋮ Theory and practice of second-order rewriting: foundation, evolution, and SOL ⋮ SOL

Uses Software

• OBJ3
• CafeOBJ
• Maude
• GHC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Notions of computation and monads
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Deterministic second-order patterns
• Higher-order rewrite systems and their confluence
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A fully abstract model for the \(\pi\)-calculus.
• Logical foundations of CafeOBJ
• Polymorphic rewrite rules: confluence, type inference, and instance validation
• Free-algebra models for the \(\pi \)-calculus
• On MacLane's conditions for coherence of natural associativities, commutativities, etc
• Two Cotensors in One: Presentations of Algebraic Theories for Local State and Fresh Names
• A reflection on call-by-value
• Algebraic Effects, Linearity, and Quantum Programming Languages
• A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems
• Associated type synonyms
• Polymorphic Abstract Syntax via Grothendieck Construction
• A Terminating and Confluent Linear Lambda Calculus
• Semantic Labelling for Proving Termination of Combinatory Reduction Systems
• Second-Order Equational Logic (Extended Abstract)
• Second-Order Algebraic Theories
• Extensional Rewriting with Sums
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Computational types from a logical perspective
• Comprehending monads
• Traced Premonoidal Categories
• Classical linear logic of implications
• Term Rewriting and All That
• Computing Tomorrow
• An Algebraic Presentation of Predicate Logic
• The Algebra of Directed Acyclic Graphs
• Just do it
• Instances of Computational Effects: An Algebraic Perspective
• Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
• Associated types with class
• Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories.
• Functions-as-constructors Higher-order Unification
• Programming Languages and Systems
• Term Rewriting and Applications
• Typed Lambda Calculi and Applications
• Logic Based Program Synthesis and Transformation

This page was built for publication: How to prove decidability of equational theories with second-order computation analyser SOL