BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Australia
1 × China
1 × Estonia
1 × Germany
1 × Japan
1 × Russia
12 × USA
2 × Denmark
3 × Italy
3 × The Netherlands
4 × United Kingdom
Collaborated with:
∅ D.v.Oheimb O.Müller Z.Qian U.Martin J.Hölzl G.Snelting D.Traytel L.Hupel F.Haftmann S.Böhme M.Wildmoser S.Berghofer F.Mehta L.P.Nieto C.Prehofer L.C.Paulson M.Eberl G.Bauer P.Schultz D.Wasserrab F.Tip J.C.Blanchette L.Noschinski J.Esparza P.Lammich R.Neumann A.Schimpf J.Smaus
Talks about:
order (8) verifi (7) isabell (6) higher (6) type (5) rewrit (4) proof (4) unif (4) hol (4) system (3)

Person: Tobias Nipkow

DBLP DBLP: Nipkow:Tobias

Facilitated 3 volumes:

FM 2006Ed
IJCAR 2001Ed
RTA 1998Ed

Contributed to:

ESOP 20152015
CAV 20132013
ICFP 20132013
TACAS 20122012
VMCAI 20122012
FLOPS 20102010
IJCAR 20102010
IJCAR 20082008
IJCAR 20062006
OOPSLA 20062006
ESOP 20052005
SEFM 20042004
CADE 20032003
CSL 20022002
FME 20022002
FoSSaCS 20012001
CADE 19991999
FASE 19991999
POPL 19981998
CADE 19961996
RTA 19951995
TACAS 19951995
POPL 19931993
TLCA 19931993
CADE 19921992
FPCA 19911991
LICS 19911991
RTA 19911991
CADE 19901990
LICS 19901990
RTA 19891989
CADE 19861986
TAPSOFT CAAP/FASE 19971997
ESOP 20182018
Haskell 20142014

Wrote 36 papers:

ESOP-2015-EberlHN #compilation #probability
A Verified Compiler for Probability Density Functions (ME, JH, TN), pp. 80–104.
CAV-2013-EsparzaLNNSS #execution #ltl #model checking
A Fully Verified Executable LTL Model Checker (JE, PL, RN, TN, AS, JGS), pp. 463–478.
ICFP-2013-TraytelN #regular expression #word
Verified decision procedures for MSO on words based on derivatives of regular expressions (DT, TN), pp. 3–12.
TACAS-2012-HolzlN #model checking #verification
Verifying pCTL Model Checking (JH, TN), pp. 347–361.
VMCAI-2012-Nipkow #education #proving #semantics
Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs (TN), pp. 24–38.
FLOPS-2010-HaftmannN #code generation #higher-order #term rewriting
Code Generation via Higher-Order Rewrite Systems (FH, TN), pp. 103–117.
IJCAR-2010-BohmeN #named
Sledgehammer: Judgement Day (SB, TN), pp. 107–121.
IJCAR-2008-Nipkow #linear #quantifier
Linear Quantifier Elimination (TN), pp. 18–33.
IJCAR-2006-NipkowBS #graph
Flyspeck I: Tame Graphs (TN, GB, PS), pp. 21–35.
OOPSLA-2006-WasserrabNST #c++ #inheritance #multi #semantics #type safety
An operational semantics and type safety prooffor multiple inheritance in C++ (DW, TN, GS, FT), pp. 345–362.
ESOP-2005-WildmoserN #bytecode #safety
Asserting Bytecode Safety (MW, TN), pp. 326–341.
SEFM-2004-BerghoferN #higher-order #random testing #testing
Random Testing in Isabelle/HOL (SB, TN), pp. 230–239.
CADE-2003-MehtaN #higher-order #logic #pointer #proving #source code
Proving Pointer Programs in Higher-Order Logic (FM, TN), pp. 121–135.
CSL-2002-Nipkow #bound #hoare #logic #nondeterminism #recursion
Hoare Logics for Recursive Procedures and Unbounded Nondeterminism (TN), pp. 103–119.
FME-2002-OheimbN #hoare #logic #revisited
Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited (DvO, TN), pp. 89–105.
FoSSaCS-2001-Nipkow #bytecode #verification
Verified Bytecode Verifiers (TN), pp. 347–363.
CADE-1999-Nipkow #programming language #proving #theorem proving
Invited Talk: Embedding Programming Languages in Theorem Provers (TN), p. 398.
FASE-1999-NipkowN #higher-order
Owicki/Gries in Isabelle/HOL (TN, LPN), pp. 188–203.
POPL-1998-NipkowO #java #type safety
JavaNone is Type-Safe — Definitely (TN, DvO), pp. 161–170.
CADE-1996-Nipkow #higher-order #proving
More Church-Rosser Proofs (in Isabelle/HOL) (TN), pp. 733–747.
RTA-1995-Nipkow #higher-order #term rewriting
Higher-Order Rewrite Systems (TN), p. 256.
TACAS-1995-MullerN #deduction #model checking
Combining Model Checking and Deduction for I/O-Automata (OM, TN), pp. 1–16.
POPL-1993-NipkowP #type checking
Type Checking Type Classes (TN, CP), pp. 409–418.
TLCA-1993-Nipkow #confluence #higher-order #orthogonal #term rewriting
Orthogonal Higher-Order Rewrite Systems are Confluent (TN), pp. 306–317.
CADE-1992-NipkowP
Isabelle-91 (TN, LCP), pp. 673–676.
CADE-1992-NipkowQ #reduction #type system #unification #λ-calculus
Reduction and Unification in Lambda Calculi with Subtypes (TN, ZQ), pp. 66–78.
FPCA-1991-NipkowS #order #unification
Type Classes and Overloading Resolution via Order-Sorted Unification (TN, GS), pp. 1–14.
LICS-1991-Nipkow #higher-order
Higher-Order Critical Pairs (TN), pp. 342–349.
RTA-1991-NipkowQ #composition #higher-order
Modular Higher-Order E-Unification (TN, ZQ), pp. 200–214.
CADE-1990-MartinN #confluence #order
Ordered Rewriting and Confluence (UM, TN), pp. 366–380.
LICS-1990-Nipkow #equation #proving
Proof Transformations for Equational Theories (TN), pp. 278–288.
RTA-1989-Nipkow #algorithm
Combining Matching Algorithms: The Rectangular Case (TN), pp. 343–358.
CADE-1986-MartinN #unification
Unification in Boolean Rings (UM, TN), pp. 506–513.
TAPSOFT-1997-MullerN #higher-order
Traces of I/O-Automata in Isabelle/HOLCF (OM, TN), pp. 580–594.
ESOP-2018-HupelN #compilation #higher-order
A Verified Compiler from Isabelle/HOL to CakeML (LH, TN), pp. 999–1026.
Haskell-2014-BlanchetteHNNT #case study #experience #haskell
Experience report: the next 1100 Haskell programmers (JCB, LH, TN, LN, DT), pp. 25–30.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.