Presenting 14 papers from the Second International Workshop on Higher-Order Algebra, Logic and Term-Rewriting, this work reports on the state of the art, addressing relevant theoretical aspects and discussing existing proof systems and term rewriting systems.

Term graph rewriting.- Approximation and normalization results for typeable term rewriting systems.- Modular properties of algebraic type systems.- Collapsing partial combinatory algebras.- A complete proof system for Nested Term Graphs.- R n - and G n -logics.- The variable containment problem.- Higher-order equational logic for specification, simulation and testing.- The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving.- Assertions and recursions.- Development closed critical pairs.- Two different strong normalization proofs?.- Third-order matching in the polymorphic lambda calculus.- Higher-order algebra with transfinite types.- Abstraction of hardware construction.

GPSR Compliance The European Union's (EU) General Product Safety Regulation (GPSR) is a set of rules that requires consumer products to be safe and our obligations to ensure this. If you have any concerns about our products you can contact us on ProductSafety@springernature.com. In case Publisher is established outside the EU, the EU authorized representative is: Springer Nature Customer Service Center GmbH Europaplatz 3 69115 Heidelberg, Germany ProductSafety@springernature.com