default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDChristian Sternagel
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2021
[j21]Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel:
Regular Tree Relations. Arch. Formal Proofs 2021 (2021)- [j20]Christian Sternagel, René Thiemann, Akihisa Yamada:
A Formalization of Weighted Path Orders and Recursive Path Orders. Arch. Formal Proofs 2021 (2021) - 2020
- [j19]Christian Sternagel, René Thiemann:
A Formalization of Knuth-Bendix Orders. Arch. Formal Proofs 2020 (2020) - [c33]René Thiemann, Jonas Schöpf
, Christian Sternagel, Akihisa Yamada:
Certifying the Weighted Path Order (Invited Talk). FSCD 2020: 4:1-4:20
2010 – 2019
- 2019
- [j18]Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler:
Abstract Completion, Formalized. Log. Methods Comput. Sci. 15(3) (2019) - [c32]Christian Sternagel, Sarah Winkler:
Certified Equational Reasoning via Ordered Completion. CADE 2019: 508-525 - [c31]Alexander Lochmann, Christian Sternagel:
Certified ACKBO. CPP 2019: 144-151 - [c30]Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, Akihisa Yamada:
The Termination and Complexity Competition. TACAS (3) 2019: 156-166 - [c29]Christian Sternagel, Akihisa Yamada:
Reachability Analysis for Termination and Confluence of Rewriting. TACAS (1) 2019: 262-278 - [c28]Florian Meßner, Christian Sternagel:
nonreach - A Tool for Nonreachability Analysis. TACAS (1) 2019: 337-343 - 2018
- [j17]Christian Sternagel, René Thiemann:
First-Order Terms. Arch. Formal Proofs 2018 (2018) - [c27]Florian Meßner, Julian Parsert, Jonas Schöpf, Christian Sternagel:
A Formally Verified Solver for Homogeneous Linear Diophantine Equations. ITP 2018: 441-458 - [i18]Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler:
Abstract Completion, Formalized. CoRR abs/1802.08437 (2018) - [i17]Christian Sternagel:
The remote_build Tool. CoRR abs/1805.07195 (2018) - [i16]Christian Sternagel, Sarah Winkler:
Certified Ordered Completion. CoRR abs/1805.10090 (2018) - [i15]Jonas Schöpf, Christian Sternagel:
TTT2 with Termination Templates for Teaching. CoRR abs/1806.05040 (2018) - 2017
- [j16]Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel:
HOLCF-Prelude. Arch. Formal Proofs 2017 (2017) - [j15]Florian Messner, Julian Parsert, Jonas Schöpf, Christian Sternagel:
Homogeneous Linear Diophantine Equations. Arch. Formal Proofs 2017 (2017) - [c26]Christian Sternagel, Thomas Sternagel:
Certifying Confluence of Quasi-Decreasing Strongly Deterministic Conditional Term Rewrite Systems. CADE 2017: 413-431 - [c25]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:
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. FroCoS 2017: 3-21 - [c24]Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler:
Infinite Runs in Abstract Completion. FSCD 2017: 19:1-19:16 - [i14]Thomas Sternagel, Christian Sternagel:
Certified Non-Confluence with ConCon 1.5. CoRR abs/1709.05162 (2017) - 2016
- [j14]Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom, Christian Sternagel:
The Z Property. Arch. Formal Proofs 2016 (2016) - [c23]Akihisa Yamada, Christian Sternagel, René Thiemann, Keiichirou Kusakari:
AC Dependency Pairs Revisited. CSL 2016: 8:1-8:16 - [c22]Christian Sternagel, Thomas Sternagel:
Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion. FSCD 2016: 29:1-29:16 - [i13]Christian Sternagel, Thomas Sternagel:
Level-Confluence of 3-CTRSs in Isabelle/HOL. CoRR abs/1602.07115 (2016) - [i12]Julian Nagele, Vincent van Oostrom, Christian Sternagel:
A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle. CoRR abs/1609.03139 (2016) - [i11]Thomas Sternagel, Christian Sternagel:
Formalized Confluence of Quasi-Decreasing, Strongly Deterministic Conditional TRSs. CoRR abs/1609.03341 (2016) - [i10]Thomas Sternagel, Christian Sternagel:
A Characterization of Quasi-Decreasingness. CoRR abs/1609.03345 (2016) - [i9]Christian Sternagel:
The Generalized Subterm Criterion in TTT2. CoRR abs/1609.03432 (2016) - 2015
- [j13]Christian Sternagel, René Thiemann:
Deriving class instances for datatypes. Arch. Formal Proofs 2015 (2015) - [c21]Christian Sternagel, René Thiemann:
Deriving Comparators and Show Functions in Isabelle/HOL. ITP 2015: 421-437 - [c20]Martin Avanzini, Christian Sternagel, René Thiemann:
Certification of Complexity Proofs using CeTA. RTA 2015: 23-39 - 2014
- [j12]Christian Sternagel:
Imperative Insertion Sort. Arch. Formal Proofs 2014 (2014) - [j11]Christian Sternagel, René Thiemann:
Haskell's Show-Class in Isabelle/HOL. Arch. Formal Proofs 2014 (2014) - [j10]Christian Sternagel, René Thiemann:
XML. Arch. Formal Proofs 2014 (2014) - [j9]Christian Sternagel, René Thiemann:
Certification Monads. Arch. Formal Proofs 2014 (2014) - [j8]Christian Sternagel:
Certified Kruskal's Tree Theorem. J. Formaliz. Reason. 7(1): 45-62 (2014) - [c19]Nao Hirokawa, Aart Middeldorp, Christian Sternagel:
A New and Formalized Proof of Abstract Completion. ITP 2014: 292-307 - [c18]Christian Sternagel, René Thiemann:
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs. RTA-TLCA 2014: 441-455 - [c17]Christian Sternagel, René Thiemann:
The Certification Problem Format. UITP 2014: 61-72 - [c16]Christian Sternagel, René Thiemann:
A Framework for Developing Stand-Alone Certifiers. LSFA 2014: 51-67 - 2013
- [j7]Christian Sternagel:
Proof Pearl - A Mechanized Proof of GHC's Mergesort. J. Autom. Reason. 51(4): 357-370 (2013) - [c15]Christian Sternagel:
Certified Kruskal's Tree Theorem. CPP 2013: 178-193 - [c14]Christian Sternagel, René Thiemann:
Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. RTA 2013: 287-302 - [i8]Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel:
Certified HLints with Isabelle/HOLCF-Prelude. CoRR abs/1306.1340 (2013) - [i7]Bertram Felgenhauer, Martin Avanzini, Christian Sternagel:
A Haskell Library for Term Rewriting. CoRR abs/1307.2328 (2013) - 2012
- [j6]Christian Sternagel:
Well-Quasi-Orders. Arch. Formal Proofs 2012 (2012) - [c13]Christian Sternagel, René Thiemann:
Certification of Nontermination Proofs. ITP 2012: 266-282 - [i6]Christian Sternagel:
A Locale for Minimal Bad Sequences. CoRR abs/1208.1366 (2012) - [i5]Christian Sternagel:
Getting Started with Isabelle/jEdit. CoRR abs/1208.1368 (2012) - [i4]Christian Sternagel, René Thiemann, Sarah Winkler, Harald Zankl:
CeTA - A Tool for Certified Termination Analysis. CoRR abs/1208.1591 (2012) - [i3]Christian Sternagel, René Thiemann:
Certification extends Termination Techniques. CoRR abs/1208.1594 (2012) - [i2]Christian Sternagel, René Thiemann:
A Relative Dependency Pair Framework. CoRR abs/1208.1595 (2012) - [i1]Thomas Sternagel, René Thiemann, Harald Zankl, Christian Sternagel:
Recording Completion for Finding and Certifying Proofs in Equational Logic. CoRR abs/1208.1597 (2012) - 2011
- [j5]Christian Sternagel:
Efficient Mergesort. Arch. Formal Proofs 2011 (2011) - [j4]Christian Sternagel, René Thiemann:
Executable Transitive Closures of Finite Relations. Arch. Formal Proofs 2011 (2011) - [c12]Christian Sternagel, René Thiemann:
Generalized and Formalized Uncurrying. FroCoS 2011: 243-258 - [c11]Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl:
Termination of Isabelle Functions via Termination of Rewriting. ITP 2011: 152-167 - [c10]Christian Sternagel, René Thiemann:
Modular and Certified Semantic Labeling and Unlabeling. RTA 2011: 329-344 - 2010
- [j3]Christian Sternagel, René Thiemann:
Abstract Rewriting. Arch. Formal Proofs 2010 (2010) - [j2]Christian Sternagel, René Thiemann:
Executable Matrix Operations on Matrices of Arbitrary Dimensions. Arch. Formal Proofs 2010 (2010) - [j1]Christian Sternagel, René Thiemann:
Executable Multivariate Polynomials. Arch. Formal Proofs 2010 (2010) - [c9]Christian Sternagel, René Thiemann:
Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs. CSL 2010: 514-528 - [c8]Christian Sternagel, René Thiemann:
Certified Subterm Criterion and Certified Usable Rules. RTA 2010: 325-340 - [c7]Harald Zankl, Christian Sternagel, Dieter Hofbauer, Aart Middeldorp:
Finding and Certifying Loops. SOFSEM 2010: 755-766 - [c6]René Thiemann, Christian Sternagel, Jürgen Giesl, Peter Schneider-Kamp:
Loops under Strategies ... Continued. IWS 2010: 51-65
2000 – 2009
- 2009
- [c5]René Thiemann, Christian Sternagel:
Loops under Strategies. RTA 2009: 17-31 - [c4]Martin Korp, Christian Sternagel, Harald Zankl, Aart Middeldorp:
Tyrolean Termination Tool 2. RTA 2009: 295-304 - [c3]René Thiemann, Christian Sternagel:
Certification of Termination Proofs Using CeTA. TPHOLs 2009: 452-468 - 2008
- [c2]Christian Sternagel, Aart Middeldorp:
Root-Labeling. RTA 2008: 336-350 - [c1]Harald Zankl, Christian Sternagel, Aart Middeldorp:
Transforming SAT into Termination of Rewriting. WFLP 2008: 199-214
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 23:00 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
