Christian Sternagel

73 papers A 2B 13Journal 40Unranked 18

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	First-Order Rewriting. Arch. Formal Proofs René Thiemann, Christian Sternagel, Christina Kirk, Martin Avanzini, Bertram Felgenhauer, Julian Nagele, Thomas Sternagel, Sarah Winkler, Akihisa Yamada
2021	J	`jnl`	A Formalization of Weighted Path Orders and Recursive Path Orders. Arch. Formal Proofs Christian Sternagel, René Thiemann, Akihisa Yamada
2021	J	`jnl`	Regular Tree Relations. Arch. Formal Proofs Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel
2020	J	`jnl`	A Formalization of Knuth-Bendix Orders. Arch. Formal Proofs Christian Sternagel, René Thiemann
2020	B	`conf`	Certifying the Weighted Path Order (Invited Talk). FSCD René Thiemann, Jonas Schöpf, Christian Sternagel, Akihisa Yamada
2019	J	`jnl`	Abstract Completion, Formalized. Log. Methods Comput. Sci. Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
2019	B	`conf`	Certified ACKBO. CPP Alexander Lochmann, Christian Sternagel
2019	A	`conf`	Certified Equational Reasoning via Ordered Completion. CADE Christian Sternagel, Sarah Winkler
2019	—	`conf`	Reachability Analysis for Termination and Confluence of Rewriting. TACAS (1) Christian Sternagel, Akihisa Yamada
2019	—	`conf`	The Termination and Complexity Competition. TACAS (3) Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada
2019	—	`conf`	nonreach - A Tool for Nonreachability Analysis. TACAS (1) Florian Meßner, Christian Sternagel
2018	B	`conf`	A Formally Verified Solver for Homogeneous Linear Diophantine Equations. ITP Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel
2018	J	`jnl`	Abstract Completion, Formalized. CoRR Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
2018	J	`jnl`	Certified Ordered Completion. CoRR Christian Sternagel, Sarah Winkler
2018	J	`jnl`	First-Order Terms. Arch. Formal Proofs Christian Sternagel, René Thiemann
2018	J	`jnl`	TTT2 with Termination Templates for Teaching. CoRR Jonas Schöpf, Christian Sternagel
2018	J	`jnl`	The remote_build Tool. CoRR Christian Sternagel
2017	J	`jnl`	Certified Non-Confluence with ConCon 1.5. CoRR Thomas Sternagel, Christian Sternagel
2017	A	`conf`	Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. CADE Christian Sternagel, Thomas Sternagel
2017	—	`conf`	Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel
2017	J	`jnl`	HOLCF-Prelude. Arch. Formal Proofs Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel
2017	J	`jnl`	Homogeneous Linear Diophantine Equations. Arch. Formal Proofs Florian Messner, Julian Parsert, Jonas Schöpf, Christian Sternagel
2017	B	`conf`	Infinite Runs in Abstract Completion. FSCD Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
2016	J	`jnl`	A Characterization of Quasi-Decreasingness. CoRR Thomas Sternagel, Christian Sternagel
2016	J	`jnl`	A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle. CoRR Julian Nagele, Vincent van Oostrom, Christian Sternagel
2016	B	`conf`	AC Dependency Pairs Revisited. CSL Akihisa Yamada, Christian Sternagel, René Thiemann, Keiichirou Kusakari
2016	B	`conf`	Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion. FSCD Christian Sternagel, Thomas Sternagel
2016	J	`jnl`	Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs. CoRR Thomas Sternagel, Christian Sternagel
2016	J	`jnl`	Level-Confluence of 3-CTRSs in Isabelle/HOL. CoRR Christian Sternagel, Thomas Sternagel
2016	J	`jnl`	The Generalized Subterm Criterion in TTT2. CoRR Christian Sternagel
2016	J	`jnl`	The Z Property. Arch. Formal Proofs Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom, Christian Sternagel
2015	—	`conf`	Certification of Complexity Proofs using CeTA. RTA Martin Avanzini, Christian Sternagel, René Thiemann
2015	B	`conf`	Deriving Comparators and Show Functions in Isabelle/HOL. ITP Christian Sternagel, René Thiemann
2015	J	`jnl`	Deriving class instances for datatypes. Arch. Formal Proofs Christian Sternagel, René Thiemann
2014	—	`conf`	A Framework for Developing Stand-Alone Certifiers. LSFA Christian Sternagel, René Thiemann
2014	B	`conf`	A New and Formalized Proof of Abstract Completion. ITP Nao Hirokawa, Aart Middeldorp, Christian Sternagel
2014	J	`jnl`	Certification Monads. Arch. Formal Proofs Christian Sternagel, René Thiemann
2014	J	`jnl`	Certified Kruskal's Tree Theorem. J. Formaliz. Reason. Christian Sternagel
2014	—	`conf`	Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs. RTA-TLCA Christian Sternagel, René Thiemann
2014	J	`jnl`	Haskell's Show-Class in Isabelle/HOL. Arch. Formal Proofs Christian Sternagel, René Thiemann
2014	J	`jnl`	Imperative Insertion Sort. Arch. Formal Proofs Christian Sternagel
2014	—	`conf`	The Certification Problem Format. UITP Christian Sternagel, René Thiemann
2014	J	`jnl`	XML. Arch. Formal Proofs Christian Sternagel, René Thiemann
2013	J	`jnl`	A Haskell Library for Term Rewriting. CoRR Bertram Felgenhauer, Martin Avanzini, Christian Sternagel
2013	J	`jnl`	Certified HLints with Isabelle/HOLCF-Prelude. CoRR Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel
2013	B	`conf`	Certified Kruskal's Tree Theorem. CPP Christian Sternagel
2013	—	`conf`	Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. RTA Christian Sternagel, René Thiemann
2013	J	`jnl`	Proof Pearl - A Mechanized Proof of GHC's Mergesort. J. Autom. Reason. Christian Sternagel
2012	J	`jnl`	A Locale for Minimal Bad Sequences CoRR Christian Sternagel
2012	J	`jnl`	A Relative Dependency Pair Framework CoRR Christian Sternagel, René Thiemann
2012	J	`jnl`	CeTA - A Tool for Certified Termination Analysis CoRR Christian Sternagel, René Thiemann, Sarah Winkler, Harald Zankl
2012	J	`jnl`	Certification extends Termination Techniques CoRR Christian Sternagel, René Thiemann
2012	B	`conf`	Certification of Nontermination Proofs. ITP Christian Sternagel, René Thiemann
2012	J	`jnl`	Getting Started with Isabelle/jEdit CoRR Christian Sternagel
2012	J	`jnl`	Recording Completion for Finding and Certifying Proofs in Equational Logic CoRR Thomas Sternagel, René Thiemann, Harald Zankl, Christian Sternagel
2012	J	`jnl`	Well-Quasi-Orders. Arch. Formal Proofs Christian Sternagel
2011	J	`jnl`	Efficient Mergesort. Arch. Formal Proofs Christian Sternagel
2011	J	`jnl`	Executable Transitive Closures of Finite Relations. Arch. Formal Proofs Christian Sternagel, René Thiemann
2011	—	`conf`	Generalized and Formalized Uncurrying. FroCoS Christian Sternagel, René Thiemann
2011	—	`conf`	Modular and Certified Semantic Labeling and Unlabeling. RTA Christian Sternagel, René Thiemann
2011	B	`conf`	Termination of Isabelle Functions via Termination of Rewriting. ITP Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl
2010	J	`jnl`	Abstract Rewriting. Arch. Formal Proofs Christian Sternagel, René Thiemann
2010	—	`conf`	Certified Subterm Criterion and Certified Usable Rules. RTA Christian Sternagel, René Thiemann
2010	J	`jnl`	Executable Matrix Operations on Matrices of Arbitrary Dimensions. Arch. Formal Proofs Christian Sternagel, René Thiemann
2010	J	`jnl`	Executable Multivariate Polynomials. Arch. Formal Proofs Christian Sternagel, René Thiemann
2010	B	`conf`	Finding and Certifying Loops. SOFSEM Harald Zankl, Christian Sternagel, Dieter Hofbauer, Aart Middeldorp
2010	—	`conf`	Loops under Strategies ... Continued IWS René Thiemann, Christian Sternagel, Jürgen Giesl, Peter Schneider-Kamp
2010	B	`conf`	Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs. CSL Christian Sternagel, René Thiemann
2009	—	`conf`	Certification of Termination Proofs Using CeTA. TPHOLs René Thiemann, Christian Sternagel
2009	—	`conf`	Loops under Strategies. RTA René Thiemann, Christian Sternagel
2009	—	`conf`	Tyrolean Termination Tool 2. RTA Martin Korp, Christian Sternagel, Harald Zankl, Aart Middeldorp
2008	—	`conf`	Root-Labeling. RTA Christian Sternagel, Aart Middeldorp
2008	—	`conf`	Transforming SAT into Termination of Rewriting. WFLP Harald Zankl, Christian Sternagel, Aart Middeldorp