Christina Kirk
Research Subjects
Christina Kirk has a total of 1 co-authors. Here are the top co-authors by number of shared publications:
- Aart Middeldorp
University of Innsbruck
2 shared publications
Latest Publications
- Open Access
- 10 January 2025
- Published by Association for Computing Machinery (ACM)
- p. 156-170
Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
We report on the formalization of a sufficient condition for confluence of first-order left-linear rewrite systems within the proof assistant Isabelle/HOL. This criterion, originally proposed by Okui (1998), is based on simultaneous critical pairs, which finitely represent peaks consisting of a multi-step and a normal step. It properly subsumes the formalized result on development-closed critical pairs.
- 10 January 2025
- Published by Association for Computing Machinery (ACM)
- p. 156-170
Open AccessFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
We report on the formalization of a sufficient condition for confluence of first-order left-linear rewrite systems within the proof assistant Isabelle/HOL. This criterion, originally proposed by Okui (1998), is based on simultaneous critical pairs, which finitely represent peaks consisting of a multi-step and a normal step. It properly subsumes the formalized result on development-closed critical pairs.
- Open Access
- 20 August 2019
- Published by Springer Nature
- p. 337-353
Composing Proof Terms
Proof terms are a useful concept for comparing computations in term rewriting. We analyze proof terms with composition, with an eye towards automation. We revisit permutation equivalence and projection equivalence, two key notions presented in the literature. We report on the integration of proof terms with composition into ProTeM, a tool for manipulating proof terms.
- 20 August 2019
- Published by Springer Nature
- p. 337-353
Open AccessComposing Proof Terms
Proof terms are a useful concept for comparing computations in term rewriting. We analyze proof terms with composition, with an eye towards automation. We revisit permutation equivalence and projection equivalence, two key notions presented in the literature. We report on the integration of proof terms with composition into ProTeM, a tool for manipulating proof terms.