220:"in recognition of his leadership in developing Isabelle and related tools, resulting in key contributions to the foundations, automation, and use of proof assistants in a wide range of applications, as well as his successful efforts in increasing the visibility of automated reasoning".
589:
387:
604:
560:
147:
316:
584:
347:
259:
579:
553:
609:
231:
151:
202:
197:
546:
184:
170:
371:
188:
192:
155:
40:
599:
210:
174:
452:
594:
166:
61:
306:
Nipkow, T. & Qian, Z. (1991). "Modular Higher-Order E-Unification". In Book, Ronald V. (ed.).
526:
294:
275:
249:(Ph.D. thesis). Computer Science Dept. Report. Vol. UMCS-87-5-3. University of Manchester.
230:
Martin, U. & Nipkow, T. (1986). "Unification in
Boolean Rings". In Jörg H. Siekmann (ed.).
343:
255:
530:
447:
437:
396:
367:
326:
Nipkow, T. (1995). "Higher-Order
Rewrite Systems (invited lecture)". In Hsiang, Jieh (ed.).
284:
143:
90:
217:
95:
573:
298:
335:
206:
383:"A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler"
466:
442:
425:
254:
Nipkow, T. (1989). "Combining
Matching Algorithms: The Rectangular Case". In
401:
382:
65:
78:
478:
289:
270:
479:"Herbrand Award for Distinguished Contributions to Automated Reasoning"
139:
72:
247:
79:
503:
271:"Unification in Primal Algebras, their Powers and their Varieties"
110:
237:
162:
57:
373:
Isabelle/HOL — A Proof
Assistant for Higher-Order Logic
359:
Rewriting
Techniques and Applications, 9th Int. Conf., RTA-98
328:
6th Int. Conf. on
Rewriting Techniques and Applications (RTA)
308:
Rewriting
Techniques and Applications, 4th Int. Conf., RTA-91
261:
Rewriting
Techniques and Applications, 3rd Int. Conf., RTA-89
180:
He is chair of the Logic and Verification group since 2011.
534:
388:
ACM Transactions on Programming Languages and Systems
318:
Proc. 6th IEEE Symposium on Logic in Computer Science
315:
Tobias Nipkow (1991). "Higher-Order Critical Pairs".
590:
Academic staff of the Technical University of Munich
105:
89:
71:
53:
36:
28:
21:
310:. LNCS. Vol. 488. Springer. pp. 200–214.
264:. LNCS. Vol. 355. Springer. pp. 343–358.
201:up to January 1, 2021. Moreover, he focuses on
173:in 1992, where he was appointed professor for
554:
330:. LNCS. Vol. 914. Springer. p. 256.
8:
240:. Vol. 230. Springer. pp. 506–513.
130:(born 1958) is a German computer scientist.
453:1871.1/1216cab9-08c1-4d41-8069-aa1735f5786d
233:Proc. 8th Conference on Automated Deduction
561:
547:
18:
451:
441:
400:
381:Gerwin Klein & Tobias Nipkow (2006).
342:. Cambridge: Cambridge University Press.
288:
525:This biographical article relating to a
605:Technische Universität Darmstadt alumni
424:Blanchette, Jasmin (12 February 2021).
416:
426:"Message from the New Editor-in-Chief"
16:German computer scientist (born 1958)
7:
514:
512:
533:. You can help Knowledge (XXG) by
14:
361:. LNCS. Vol. 1379. Springer.
154:in 1982, and his Ph.D. from the
585:Theoretical computer scientists
152:Technische Hochschule Darmstadt
430:Journal of Automated Reasoning
203:programming language semantics
198:Journal of Automated Reasoning
148:Department of Computer Science
1:
357:Nipkow, Tobias, ed. (1998).
183:He is known for his work in
340:Term Rewriting and All That
195:; he was the editor of the
171:Technical University Munich
626:
580:German computer scientists
511:
443:10.1007/s10817-021-09587-y
338:and Tobias Nipkow (1998).
189:automatic theorem proving
101:
46:
610:Computer scientist stubs
193:Isabelle proof assistant
191:, in particular for the
156:University of Manchester
41:Isabelle proof assistant
402:10.1145/1146809.1146811
370:and Wenzel M. (2002).
269:Tobias Nipkow (1990).
245:Tobias Nipkow (1987).
211:functional programming
165:from 1987, changed to
224:Selected publications
167:Cambridge University
138:Nipkow received his
62:Cambridge University
321:. pp. 342–349.
290:10.1145/96559.96569
216:In 2021 he won the
527:computer scientist
276:Journal of the ACM
175:programming theory
542:
541:
349:978-0-521-45520-6
256:Nachum Dershowitz
125:
124:
48:Scientific career
617:
563:
556:
549:
518:P ≟ NP
513:
491:
490:
488:
486:
475:
469:
464:
458:
457:
455:
445:
421:
406:
404:
377:
362:
353:
331:
322:
311:
302:
292:
265:
250:
241:
169:in 1989, and to
144:computer science
121:
118:
116:
114:
112:
91:Doctoral advisor
85:
19:
625:
624:
620:
619:
618:
616:
615:
614:
570:
569:
568:
567:
520:
509:
500:
495:
494:
484:
482:
477:
476:
472:
465:
461:
423:
422:
418:
413:
380:
365:
356:
350:
334:
325:
314:
305:
268:
253:
244:
229:
226:
136:
109:
83:
24:
17:
12:
11:
5:
623:
621:
613:
612:
607:
602:
597:
592:
587:
582:
572:
571:
566:
565:
558:
551:
543:
540:
539:
522:
516:
507:
506:
499:
498:External links
496:
493:
492:
470:
459:
415:
414:
412:
409:
408:
407:
395:(4): 619–695.
378:
366:Nipkow T. and
363:
354:
348:
332:
323:
312:
303:
283:(4): 742–776.
266:
251:
242:
225:
222:
218:Herbrand Award
135:
132:
123:
122:
107:
103:
102:
99:
98:
96:Cliff B. Jones
93:
87:
86:
75:
69:
68:
55:
51:
50:
44:
43:
38:
37:Known for
34:
33:
30:
26:
25:
22:
15:
13:
10:
9:
6:
4:
3:
2:
622:
611:
608:
606:
603:
601:
600:Living people
598:
596:
593:
591:
588:
586:
583:
581:
578:
577:
575:
564:
559:
557:
552:
550:
545:
544:
538:
536:
532:
528:
523:
519:
515:
510:
505:
502:
501:
497:
480:
474:
471:
468:
463:
460:
454:
449:
444:
439:
435:
431:
427:
420:
417:
410:
403:
398:
394:
390:
389:
384:
379:
375:
374:
369:
364:
360:
355:
351:
345:
341:
337:
333:
329:
324:
320:
319:
313:
309:
304:
300:
296:
291:
286:
282:
278:
277:
272:
267:
263:
262:
257:
252:
248:
243:
239:
235:
234:
228:
227:
223:
221:
219:
214:
212:
208:
204:
200:
199:
194:
190:
186:
181:
178:
176:
172:
168:
164:
161:He worked at
159:
157:
153:
149:
145:
141:
133:
131:
129:
128:Tobias Nipkow
120:
108:
104:
100:
97:
94:
92:
88:
81:
80:
76:
74:
70:
67:
63:
59:
56:
52:
49:
45:
42:
39:
35:
31:
27:
23:Tobias Nipkow
20:
535:expanding it
524:
517:
508:
483:. Retrieved
473:
462:
433:
429:
419:
392:
386:
372:
358:
339:
336:Franz Baader
327:
317:
307:
280:
274:
260:
246:
232:
215:
207:type systems
196:
182:
179:
160:
137:
127:
126:
77:
54:Institutions
47:
595:1958 births
376:. Springer.
185:interactive
574:Categories
481:. CADE Inc
467:Brief vita
436:(2): 155.
411:References
368:Paulson L.
504:Home page
158:in 1987.
146:from the
142:(MSc) in
66:TU Munich
299:14940917
119:/~nipkow
485:14 July
258:(ed.).
150:of the
106:Website
521:
346:
297:
140:Diplom
134:Career
84:(1987)
82:
73:Thesis
529:is a
295:S2CID
111:www21
531:stub
487:2021
344:ISBN
238:LNCS
209:and
187:and
115:.tum
32:1958
29:Born
448:hdl
438:doi
397:doi
285:doi
163:MIT
117:.de
113:.in
58:MIT
576::
446:.
434:65
432:.
428:.
393:28
391:.
385:.
293:.
281:37
279:.
273:.
236:.
213:.
205:,
177:.
64:,
60:,
562:e
555:t
548:v
537:.
489:.
456:.
450::
440::
405:.
399::
352:.
301:.
287::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.