Christian Sternagel

Journal Articles

Papers in Proceedings

Thesis

Others

Drafts

Alphabetical List of Titles

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

Valid XHTML 1.0!