担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）

The aim of this paper is to establish theoretical foundations of GHC’s rewrite rules. The Glasgow Haskell Compiler (GHC) has the feature of rewrite rules to specify optimising transformations. Rewrite rules have been widely used in many libraries. However, there has been no theory to formalise the rules and establish their correctness. We present System F<inf>RE</inf>—the polymorphic λ-calculus System F<inf>ω</inf> extended with higher-order term rewriting and equational reasoning to model GHC’s rewrite rules. We develop a theory and methods for verifying correctness of rewrite rules. The key to our method is to guarantee the rewriting properties of local confluence and strong normalisation. We prove the Rule Meaning Preservation Theorem that gives a simple criterion for establishing correctness of rewrite rules, which is suited for mechanical checking.

DOI： 10.1007/978-3-031-69042-6_5

Scopus

その他リンク： https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85203137220&origin=inward

担当区分：最終著者,　責任著者   記述言語：英語   掲載種別：研究論文（学術雑誌）

For a programming language, there are two kinds of term rewriting: run-time rewriting (“evaluation”) and compile-time rewriting (“refinement”). Whereas refinement resembles general term rewriting, evaluation is commonly constrained by Felleisen’s evaluation contexts. While evaluation specifies a programming language, refinement models optimisation and should be validated with respect to evaluation. Such validation can be given by Sands’ notion of contextual improvement. We formulate evaluation in a term-rewriting-theoretic manner for the first time, and introduce Term Evaluation and Refinement Systems (TERS). We then identify sufficient conditions for contextual improvement, and provide critical pair analysis for local coherence that is the key sufficient condition. As case studies, we prove contextual improvement for a computational lambda-calculus and its extension with effect handlers.

DOI： 10.1007/978-981-97-2300-3_3

Scopus

その他リンク： https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85194818397&origin=inward

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）

By using algebraic structures in a presheaf category over finite sets, following Fiore, Plotkin and Turi, we develop sound and complete models of second-order rewriting systems called second-order computation systems (CSs). Restricting the algebraic structures to those equipped with well-founded relations, we obtain a complete characterisation of terminating CSs. We also extend the characterisation to rewriting on meta-terms using the notion of -monoid.

DOI： 10.1017/S0960129522000287

Scopus

その他リンク： https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85144461707&origin=inward

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）

We present a new modular proof method of termination for second-order computation, and report its implementation SOL. The proof method is useful for proving termination of higher-order foundational calculi. To establish the method, we use a variation of the semantic labelling translation and Blanqui’s General Schema: a syntactic criterion of strong normalisation. an application, we show termination of a variant of call-by-push-value calculus with algebraic effects, an effect handler and effect theory. We also show that our tool SOL is effective to solve higher-order termination problems.

DOI： 10.46298/lmcs-18(2:18)2022

Scopus

その他リンク： https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85133171066&origin=inward

担当区分：最終著者,　責任著者   記述言語：英語   掲載種別：研究論文（学術雑誌）

We present a tool GSOL, a confluence checker for GHC. It checks the confluence property for rewrite rules in a Haskell program by using the confluence checker SOL (Second-Order Laboratory). The Glasgow Haskell Compiler (GHC) allows programmers to use rewrite rules to optimize Haskell programs in the compilation pipeline. Currently, GHC does not check the confluence of the user-defined rewrite rules. If the rewrite rules are not confluent then the optimization using these rules may produce unexpected results. Therefore, checking the confluence of rewrite rules is important. We implement GSOL using the plugin mechanism of GHC. and provide three usages. We demonstrate confluence checking in the Arrow library.

DOI： 10.11309/jssst.39.3_82

Scopus

その他リンク： https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=85141247947&origin=inward