Die Lösung der POPLMARK-Challenge: Neue Techniken zur maschinellen Verifikation der Korrektheit von Programmiersprachen

• Applicant: Dr. Christian Urban
• Subject Area: Theoretical Computer Science
• Term: from 2006 to 2015
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 18284775

• Final Report Year: 2016

Final Report Abstract

No abstract available

Publications

• A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. In Proc. of the 3rd International Joint Conference on Automated Reasoning (IJCAR’06), Springer Verlag, volume 4130 of LNCS, Pages 498–512, 2006
  C. Urban and S. Berghofer
  
• Barendregt’s Variable Convention in Rule Inductions. In Proc. of the 21th International Conference on Automated Deduction (CADE’07), Springer-Verlag, volume 4603 of LNCS, Pages 35–50, 2007
  C. Urban, M. Norrish and S. Berghofer
  
• Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. In Proc. of the 9th International Conference on Artificial Intelligence and Symbolic Computation (AISC’08), Springer Verlag, volume 5144 of LNAI, Pages 38–52, 2008
  P. Chapman, J. McKinna and C. Urban
  
• Mechanizing the Metatheory of LF. In Proc. of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS’08), Pages 45–56, 2008
  C. Urban, J. Cheney and S. Berghofer
  
• Nominal Inversion Principles. In Proc. of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs’08), Springer Verlag, volume 5170 of LNCS, Pages 71– 85, 2008
  S. Berghofer and C. Urban
  
• Nominal Logic Programming, ACM Transactions on Programming Languages and Systems, 30(5), Article No. 26, pages 1-47, 2008
  J. Cheney and C. Urban
  
• Nominal Techniques in Isabelle/HOL, Journal of Automated Reasoning, 40(4):327–356, 2008
  C. Urban
  
• Revisiting Cut-Elimination: One Difficult Proof is Really a Proof. In Proc. of the 19th International Conference on Rewriting Techniques and Applications (RTA’08), Springer Verlag, volume 5117 of LNCS, Pages 409–424, 2008
  C. Urban and B. Zhu
  
• A New Foundation for Nominal Isabelle. In Proc. of the 1st Conference on Interactive Theorem Proving (ITP’10), Springer Verlag, volume 6172 of LNCS, Pages 35–50, 2010
  B. Huffman and C. Urban
  
• General Bindings and Alpha-Equivalence in Nominal Isabelle. In Proc. of the 20th European Symposium on Programming (ESOP’11), Springer Verlag, volume 6602 of LNCS, Pages 480-500, 2011
  C. Urban and C. Kaliszyk
  
• Mechanizing the Metatheory of LF, ACM Transactions on Computational Logic, 12(2):15:1–15:42, 2011
  C. Urban, J. Cheney and S. Berghofer
  
• Mechanizing the Metatheory of Mini-XQuery. In Proc. of the 1st International Conference on Certified Programs and Proofs (CPP’11), Springer Verlag, volume 7086 of LNCS, Pages 280– 295, 2011
  J. Cheney and C. Urban
  
• Quotients Revisited for Isabelle/HOL. In Proc. of the 2011 ACM Symposium on Applied Computing (SAC’11), Pages 1639–1644, 2011
  C. Kaliszyk and C. Urban
  
• General Bindings and Alpha-Equivalence in Nominal Isabelle. Journal of Logical Methods in Computer Science, 8(2:14), 1–35, 2012
  C. Urban and C. Kaliszyk