default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDRené Thiemann
- > Home > Persons > René Thiemann
Publications
- 2021
[j48]Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, Thomas Sternagel:
Regular Tree Relations. Arch. Formal Proofs 2021 (2021)- [j47]Christian Sternagel, René Thiemann, Akihisa Yamada:
A Formalization of Weighted Path Orders and Recursive Path Orders. Arch. Formal Proofs 2021 (2021) - 2020
- [j43]Christian Sternagel, René Thiemann:
A Formalization of Knuth-Bendix Orders. Arch. Formal Proofs 2020 (2020) - [c54]René Thiemann, Jonas Schöpf
, Christian Sternagel, Akihisa Yamada:
Certifying the Weighted Path Order (Invited Talk). FSCD 2020: 4:1-4:20 - 2018
- [j33]Christian Sternagel, René Thiemann:
First-Order Terms. Arch. Formal Proofs 2018 (2018) - 2017
- [c45]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 - 2016
- [c43]Akihisa Yamada, Christian Sternagel, René Thiemann, Keiichirou Kusakari:
AC Dependency Pairs Revisited. CSL 2016: 8:1-8:16 - 2015
- [j24]Christian Sternagel, René Thiemann:
Deriving class instances for datatypes. Arch. Formal Proofs 2015 (2015) - [c39]Christian Sternagel, René Thiemann:
Deriving Comparators and Show Functions in Isabelle/HOL. ITP 2015: 421-437 - [c38]Martin Avanzini, Christian Sternagel, René Thiemann:
Certification of Complexity Proofs using CeTA. RTA 2015: 23-39 - 2014
- [j21]Christian Sternagel, René Thiemann:
Haskell's Show-Class in Isabelle/HOL. Arch. Formal Proofs 2014 (2014) - [j20]Christian Sternagel, René Thiemann:
XML. Arch. Formal Proofs 2014 (2014) - [j19]Christian Sternagel, René Thiemann:
Certification Monads. Arch. Formal Proofs 2014 (2014) - [c34]Christian Sternagel, René Thiemann:
Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs. RTA-TLCA 2014: 441-455 - [c32]Christian Sternagel, René Thiemann:
The Certification Problem Format. UITP 2014: 61-72 - [c31]Christian Sternagel, René Thiemann:
A Framework for Developing Stand-Alone Certifiers. LSFA 2014: 51-67 - 2013
- [c29]Christian Sternagel, René Thiemann:
Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion. RTA 2013: 287-302 - 2012
- [c28]Christian Sternagel, René Thiemann:
Certification of Nontermination Proofs. ITP 2012: 266-282 - [i12]Christian Sternagel, René Thiemann, Sarah Winkler, Harald Zankl:
CeTA - A Tool for Certified Termination Analysis. CoRR abs/1208.1591 (2012) - [i11]Christian Sternagel, René Thiemann:
Certification extends Termination Techniques. CoRR abs/1208.1594 (2012) - [i10]Christian Sternagel, René Thiemann:
A Relative Dependency Pair Framework. CoRR abs/1208.1595 (2012) - [i9]Thomas Sternagel, René Thiemann, Harald Zankl, Christian Sternagel:
Recording Completion for Finding and Certifying Proofs in Equational Logic. CoRR abs/1208.1597 (2012) - 2011
- [j11]Christian Sternagel, René Thiemann:
Executable Transitive Closures of Finite Relations. Arch. Formal Proofs 2011 (2011) - [c26]Christian Sternagel, René Thiemann:
Generalized and Formalized Uncurrying. FroCoS 2011: 243-258 - [c25]Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs, Jürgen Giesl:
Termination of Isabelle Functions via Termination of Rewriting. ITP 2011: 152-167 - [c24]Christian Sternagel, René Thiemann:
Modular and Certified Semantic Labeling and Unlabeling. RTA 2011: 329-344 - 2010
- [j9]Christian Sternagel, René Thiemann:
Abstract Rewriting. Arch. Formal Proofs 2010 (2010) - [j8]Christian Sternagel, René Thiemann:
Executable Matrix Operations on Matrices of Arbitrary Dimensions. Arch. Formal Proofs 2010 (2010) - [j7]Christian Sternagel, René Thiemann:
Executable Multivariate Polynomials. Arch. Formal Proofs 2010 (2010) - [c23]Christian Sternagel, René Thiemann:
Signature Extensions Preserve Termination - An Alternative Proof via Dependency Pairs. CSL 2010: 514-528 - [c22]Christian Sternagel, René Thiemann:
Certified Subterm Criterion and Certified Usable Rules. RTA 2010: 325-340 - [c21]René Thiemann, Christian Sternagel, Jürgen Giesl, Peter Schneider-Kamp:
Loops under Strategies ... Continued. IWS 2010: 51-65 - 2009
- [c20]René Thiemann, Christian Sternagel:
Loops under Strategies. RTA 2009: 17-31 - [c18]René Thiemann, Christian Sternagel:
Certification of Termination Proofs Using CeTA. TPHOLs 2009: 452-468
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-08-22 20:47 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:
