Foto von Tobias Nipkow

Scopus-Profil ansehen

Tobias Nipkow

Prof.

 https://orcid.org/0000-0003-0730-515X
1982 …2024

Publikationen pro Jahr

Filter
Konferenzbeitrag

Suchergebnisse

  • 2024

    Alpha-Beta Pruning Verified

    Nipkow, T., Sept. 2024, 15th International Conference on Interactive Theorem Proving, ITP 2024. Bertot, Y., Kutsia, T. & Norrish, M. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 1. (Leibniz International Proceedings in Informatics, LIPIcs; Band 309).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

  • A Verified Earley Parser

    Rau, M. & Nipkow, T., Sept. 2024, 15th International Conference on Interactive Theorem Proving, ITP 2024. Bertot, Y., Kutsia, T. & Norrish, M. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 31. (Leibniz International Proceedings in Informatics, LIPIcs; Band 309).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

  • 2023

    Real-Time Double-Ended Queue Verified (Proof Pearl)

    Toth, B. & Nipkow, T., Juli 2023, 14th International Conference on Interactive Theorem Proving, ITP 2023. Naumowicz, A. & Thiemann, R. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 29. (Leibniz International Proceedings in Informatics, LIPIcs; Band 268).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

  • Verification of NP-Hardness Reduction Functions for Exact Lattice Problems

    Kreuzer, K. & Nipkow, T., 2023, Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings. Pientka, B. & Tinelli, C. (Hrsg.). Springer Science and Business Media Deutschland GmbH, S. 365-381 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 14132 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    2 Zitate (Scopus)
  • 2022

    A Verified Implementation of B + -Trees in Isabelle/HOL

    Mündler, N. & Nipkow, T., 2022, Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. Seidl, H., Liu, Z. & Pasareanu, C. S. (Hrsg.). Springer Science and Business Media Deutschland GmbH, S. 324-341 18 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 13572 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
  • 2021

    A Verified Decision Procedure for Orders in Isabelle/HOL

    Stevens, L. & Nipkow, T., 2021, Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings. Hou, Z. & Ganesh, V. (Hrsg.). Springer Science and Business Media Deutschland GmbH, S. 127-143 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12971 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    1 Zitat (Scopus)

  • Isabelle’s Metalogic: Formalization and Proof Checker

    Nipkow, T. & Roßkopf, S., 2021, Automated Deduction – CADE 28 - 28th International Conference on Automated Deduction, 2021, Proceedings. Platzer, A. & Sutcliffe, G. (Hrsg.). Springer Science and Business Media Deutschland GmbH, S. 93-110 18 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12699 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    9 Zitate (Scopus)

  • Teaching algorithms and data structures with a proof assistant (invited talk)

    Nipkow, T., 17 Jan. 2021, CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. Hritcu, C. & Popescu, A. (Hrsg.). Association for Computing Machinery, Inc, S. 1-3 3 S. (CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    2 Zitate (Scopus)
  • 2020

    Proof pearl: Braun trees

    Nipkow, T. & Sewell, T., 20 Jan. 2020, CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020. Blanchette, J. & Hritcu, C. (Hrsg.). Association for Computing Machinery, Inc, S. 18-31 14 S. (CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    1 Zitat (Scopus)

  • Verification of Closest Pair of Points Algorithms

    Rau, M. & Nipkow, T., 2020, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings. Peltier, N. & Sofronie-Stokkermans, V. (Hrsg.). Springer, S. 341-357 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12167 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    1 Zitat (Scopus)

  • Verified Approximation Algorithms

    Eßmann, R., Nipkow, T. & Robillard, S., 2020, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings. Peltier, N. & Sofronie-Stokkermans, V. (Hrsg.). Springer, S. 291-306 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12167 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    3 Zitate (Scopus)

  • Verified Textbook Algorithms: A Biased Survey

    Nipkow, T., Eberl, M. & Haslbeck, M. P. L., 2020, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. Hung, D. V. & Sokolsky, O. (Hrsg.). Springer Science and Business Media Deutschland GmbH, S. 25-53 29 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12302 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    8 Zitate (Scopus)
  • 2019

    Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra

    Lammich, P. & Nipkow, T., Sept. 2019, 10th International Conference on Interactive Theorem Proving, ITP 2019. Harrison, J., O'Leary, J. & Tolmach, A. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 23. (Leibniz International Proceedings in Informatics, LIPIcs; Band 141).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    4 Zitate (Scopus)

  • Trustworthy graph algorithms

    Abdulaziz, M., Mehlhorn, K. & Nipkow, T., Aug. 2019, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019. Katoen, J.-P., Heggernes, P. & Rossmanith, P. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 1. (Leibniz International Proceedings in Informatics, LIPIcs; Band 138).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    6 Zitate (Scopus)
  • 2018

    A verified compiler from isabelle/HOL to CakeML

    Hupel, L. & Nipkow, T., 2018, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Ahmed, A. (Hrsg.). Springer Verlag, S. 999-1026 28 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10801 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    29 Zitate (Scopus)

  • Hoare logics for time bounds: A study in meta theory

    Haslbeck, M. P. L. & Nipkow, T., 2018, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Beyer, D. & Huisman, M. (Hrsg.). Springer Verlag, S. 155-171 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10805 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    11 Zitate (Scopus)

  • Verified Analysis of Random Binary Tree Structures

    Eberl, M., Haslbeck, M. W. & Nipkow, T., 2018, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Avigad, J. & Mahboubi, A. (Hrsg.). Springer Verlag, S. 196-214 19 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10895 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    4 Zitate (Scopus)

  • Verified Memoization and Dynamic Programming

    Wimmer, S., Hu, S. & Nipkow, T., 2018, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Avigad, J. & Mahboubi, A. (Hrsg.). Springer Verlag, S. 579-596 18 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10895 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    5 Zitate (Scopus)
  • 2017

    Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL

    Rizaldi, A., Keinholz, J., Huber, M., Feldle, J., Immler, F., Althoff, M., Hilgendorf, E. & Nipkow, T., 2017, Integrated Formal Methods - 13th International Conference, IFM 2017, Proceedings. Schneider, S. & Polikarpova, N. (Hrsg.). Springer Verlag, S. 50-66 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10510 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    67 Zitate (Scopus)

  • Formalized Proof Systems for Propositional Logic

    Michaelis, J. & Nipkow, T., 2017, 23rd International Conference on Types for Proofs and Programs, TYPES 2017. Kaposi, A. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 5. (Leibniz International Proceedings in Informatics, LIPIcs; Band 104).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    13 Zitate (Scopus)

  • Verified root-balanced trees

    Nipkow, T., 2017, Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Proceedings. Chang, B.-Y. E. (Hrsg.). Springer Verlag, S. 255-272 18 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 10695 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    9 Zitate (Scopus)
  • 2016

    Automatic functional correctness proofs for functional search trees

    Nipkow, T., 2016, Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. Blanchette, J. C. & Merz, S. (Hrsg.). Springer Verlag, S. 307-322 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 9807 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    10 Zitate (Scopus)

  • Verified Analysis of Functional Data Structures

    Nipkow, T., 1 Juni 2016, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. Kesner, D. & Pientka, B. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 4. (Leibniz International Proceedings in Informatics, LIPIcs; Band 52).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    2 Zitate (Scopus)

  • Verified analysis of list update algorithms

    Haslbeck, M. P. L. & Nipkow, T., 1 Dez. 2016, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016. Lal, A., Akshay, S., Saurabh, S., Sen, S. & Saurabh, S. (Hrsg.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, S. 49.1-49.15 (Leibniz International Proceedings in Informatics, LIPIcs; Band 65).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    1 Zitat (Scopus)
  • 2015

    Amortized complexity verified

    Nipkow, T., 2015, Interactive Theorem Proving - 6th International Conference, ITP 2015, Proceedings. Zhang, X. & Urban, C. (Hrsg.). Springer Verlag, S. 310-324 15 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 9236).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    19 Zitate (Scopus)

  • A verified compiler for probability density functions

    Eberl, M., Hölzl, J. & Nipkow, T., 2015, Programming Languages and Systems - 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Vitek, J. (Hrsg.). Springer Verlag, S. 80-104 25 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 9032).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    21 Zitate (Scopus)

  • Mining the archive of formal proofs

    Blanchette, J. C., Haslbeck, M., Matichuk, D. & Nipkow, T., 2015, Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings. Kerber, M., Sorge, V., Rabe, F., Carette, J. & Kaliszyk, C. (Hrsg.). Springer Verlag, S. 3-17 15 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 9150).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    32 Zitate (Scopus)
  • 2014

    Experience report: The next 1100 Haskell programmers

    Blanchette, J. C., Hupel, L., Nipkow, T., Noschinski, L. & Traytel, D., 2014, Haskell 2014 - Proceedings of the 2014 ACM SIGPLAN Haskell Symposium. Association for Computing Machinery, S. 25-30 6 S. (Haskell 2014 - Proceedings of the 2014 ACM SIGPLAN Haskell Symposium).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

  • Unified decision procedures for regular expression equivalence

    Nipkow, T. & Traytel, D., 2014, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, S. 450-466 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 8558 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    19 Zitate (Scopus)
  • 2013

    A brief survey of verified decision procedures for equivalence of regular expressions

    Nipkow, T. & Haslbeck, M., 2013, Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings. S. 10-12 3 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 8123 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

  • A fully verified executable LTL model checker

    Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A. & Smaus, J. G., 2013, Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings. S. 463-478 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 8044 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    72 Zitate (Scopus)

  • Data refinement in Isabelle/HOL

    Haftmann, F., Krauss, A., Kunčar, O. & Nipkow, T., 2013, Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. S. 100-115 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 7998 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    49 Zitate (Scopus)

  • Formalizing probabilistic noninterference

    Popescu, A., Hol̈zl, J. & Nipkow, T., 2013, Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings. S. 259-275 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 8307 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    9 Zitate (Scopus)

  • Noninterfering schedulers when possibilistic noninterference implies probabilistic noninterference

    Popescu, A., Hölzl, J. & Nipkow, T., 2013, Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings. Springer Verlag, S. 236-252 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 8089 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    5 Zitate (Scopus)

  • Verified decision procedures for MSO on words based on derivatives of regular expressions

    Traytel, D. & Nipkow, T., 2013, ICFP 2013 - Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming. S. 3-12 10 S. (Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    4 Zitate (Scopus)
  • 2012

    Abstract interpretation of annotated commands

    Nipkow, T., 2012, Interactive Theorem Proving - Third International Conference, ITP 2012, Proceedings. S. 116-132 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 7406 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    10 Zitate (Scopus)

  • Proving concurrent noninterference

    Popescu, A., Hölzl, J. & Nipkow, T., 2012, Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings. S. 109-125 17 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 7679 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    9 Zitate (Scopus)

  • Teaching semantics with a proof assistant: No more LSD trip proofs

    Nipkow, T., 2012, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings. S. 24-38 15 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 7148 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    23 Zitate (Scopus)

  • Verifying pCTL model checking

    Hölzl, J. & Nipkow, T., 2012, Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings. S. 347-361 15 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 7214 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    5 Zitate (Scopus)
  • 2011

    Automatic proof and disproof in Isabelle/HOL

    Blanchette, J. C., Bulwahn, L. & Nipkow, T., 2011, Frontiers of Combining Systems - 8th International Symposium, FroCoS 2011, Proceedings. S. 12-27 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 6989 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    70 Zitate (Scopus)

  • Extending hindley-milner type inference with coercive structural subtyping

    Traytel, D., Berghofer, S. & Nipkow, T., 2011, Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Proceedings. S. 89-104 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 7078 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    12 Zitate (Scopus)

  • Proof pearl: The marriage theorem

    Jiang, D. & Nipkow, T., 2011, Certified Programs and Proofs - First International Conference, CPP 2011, Proceedings. S. 394-399 6 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 7086 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    1 Zitat (Scopus)

  • Verified efficient enumeration of plane graphs modulo isomorphism

    Nipkow, T., 2011, Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings. S. 281-296 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 6898 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    7 Zitate (Scopus)
  • 2010

    Code generation via higher-order rewrite systems

    Haftmann, F. & Nipkow, T., 2010, Functional and Logic Programming - 10th International Symposium, FLOPS 2010, Proceedings. S. 103-117 15 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 6009 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    Open Access
    138 Zitate (Scopus)

  • Nitpick: A counterexample generator for higher-order logic based on a relational model finder

    Blanchette, J. C. & Nipkow, T., 2010, Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings. S. 131-146 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 6172 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    164 Zitate (Scopus)

  • Sledgehammer: Judgement day

    Böhme, S. & Nipkow, T., 2010, Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings. S. 107-121 15 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 6173 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    84 Zitate (Scopus)
  • 2008

    A compiled implementation of normalization by evaluation

    Aehlig, K., Haftmann, F. & Nipkow, T., 2008, Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Springer Verlag, S. 39-54 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 5170 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    9 Zitate (Scopus)

  • Linear quantifier elimination

    Nipkow, T., 2008, Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings. S. 18-33 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 5195 LNAI).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    16 Zitate (Scopus)

  • The isabelle framework

    Wenzel, M., Paulson, L. C. & Nipkow, T., 2008, Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Springer Verlag, S. 33-38 6 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 5170 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    107 Zitate (Scopus)
  • 2007

    Finding lexicographic orders for termination proofs in Isabelle/HOL

    Bulwahn, L., Krauss, A. & Nipkow, T., 2007, Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings. Springer Verlag, S. 38-53 16 S. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 4732 LNCS).

    Publikation: Beitrag in Buch/Bericht/Konferenzband › Konferenzbeitrag › Begutachtung

    20 Zitate (Scopus)