Christian Sternagel

General Information

visiting researcher

address: School of Information Science
Japan Advanced Institute of Science and Technology
1-1 Asahidai, Nomi, Ishikawa, 923-1292, Japan
email: c-sterna@jaist.ac.jp
research group: Ogawa-Hirokawa Laboratory (room I-51)
 
research interests: interactive theorem proving
verification of (functional) programs
term rewriting (termination and certification of termination proofs)
ttt2   IsaFoR/CeTA
events: HART 2014 RTA-TLCA 2014 WST 2014 39th TRS Meeting HART 2013

Publications

Journal Articles

Papers in Proceedings

Thesis

Others

Drafts

Software

ttt2 A termination tool, which automatically generates a termination certificate for a given term rewrite system.
 
IsaFoR/CeTA IsaFoR is an Isabelle/HOL formalization of term rewriting and many facts about termination.
CeTA is a verified certifier (for termination certificates) and code-generated from IsaFoR.