Christian Sternagel

Journal Articles

Papers in Proceedings

Thesis

Others

Drafts

Alphabetical List of Titles

  1. A Characterization of Quasi-Decreasingness
  2. A Framework for Developing Stand-Alone Certifiers
  3. A Haskell Library for Term Rewriting
  4. A Locale for Minimal Bad Sequences
  5. A New and Formalized Proof of Abstract Completion
  6. A Relative Dependency Pair Framework
  7. A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle
  8. AC Dependency Pairs Revisited
  9. Abstract Rewriting
  10. Automatic Certification of Termination Proofs
  11. CeTA - A Tool for Certified Termination Analysis
  12. Certification Monads
  13. Certification extends Termination Techniques
  14. Certification of Complexity Proofs using CeTA
  15. Certification of Nontermination Proofs
  16. Certification of Termination Proofs using CeTA
  17. Certified HLints with Isabelle/HOLCF-Prelude
  18. Certified Kruskal's Tree Theorem
  19. Certified Kruskal's Tree Theorem
  20. Certified Non-Confluence with ConCon 1.5
  21. Certified Subterm Criterion and Certified Usable Rules
  22. Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion
  23. Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems
  24. CoCo 2015 Participant: CeTA 2.21
  25. CoCo 2016 Participant: CeTA 2.28
  26. CoCo 2017 Participant: CeTA 2.31
  27. Deriving Comparators and Show Functions in Isabelle/HOL
  28. Deriving class instances for datatypes
  29. Efficient Mergesort
  30. Executable Matrix Operations on Matrices of Arbitrary Dimensions
  31. Executable Multivariate Polynomials
  32. Executable Transitive Closures of Finite Relations
  33. Finding and Certifying Loops
  34. Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs
  35. Formalized Ground Completion
  36. Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion
  37. Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
  38. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
  39. Generalized and Formalized Uncurrying
  40. Getting Started with Isabelle/jEdit
  41. HOLCF-Prelude
  42. Haskell's Show Class in Isabelle/HOL
  43. Homogeneous Linear Diophantine Equations
  44. Imperative Insertion Sort
  45. Infinite Runs in Abstract Completion
  46. Level-Confluence of 3-CTRSs in Isabelle/HOL
  47. Loops under Strategies
  48. Loops under Strategies ... Continued
  49. Loops under Strategies ... Continued
  50. Modular and Certified Semantic Labeling and Unlabeling
  51. Normalization Equivalence of Rewrite Systems
  52. Open Induction
  53. Proof Pearl - A Mechanized Proof of GHC's Mergesort
  54. Recording Completion for Finding and Certifying Proofs in Equational Logic
  55. Root-Labeling
  56. Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs
  57. TTT2 @ TermComp'2016
  58. Termination of Isabelle Functions via Termination of Rewriting
  59. The Certification Problem Format
  60. The Generalized Subterm Criterion in TTT2
  61. The Z Property
  62. Transforming SAT into Termination of Rewriting
  63. Tyrolean Termination Tool 2
  64. Well-Quasi-Orders
  65. Xml

Valid HTML 4.01 Strict