Visiting guests
| name | affiliation | time | project |
|---|---|---|---|
| Kei Shirakizawa | JAIST | 2018, 6 June – 2019, 14 May | FORTissimo |
| Satoshi Tojo | JAIST | 2018, June 18 – 19 | – |
| Nguyen Le Minh | JAIST | 2018, June 18 | – |
| Julien Braine | ENS Lyon | 2018, March 5 – August 6 | – |
| Ryota Nakayama | Nagoya University | 2018, March 18 – 25 | – |
| Naoki Nishida | Nagoya University | 2018, March 18 – 25 | – |
| Masahiko Sakai | Nagoya University | 2018, March 18 – 21 | – |
| Anders Schlichtkrull | Technical University of Denmark | 2018, February 25 – March 3 | Certification Redux |
| Lasse Blaauwbroek | Czech Technical University in Prague | 2018, February 1 – March 2 | Strong Modular Proof Assistance |
| Josef Urban | Czech Technical University in Prague | 2018, February 19 – 23 | Strong Modular Proof Assistance |
| Cody Roux | Charles Stark Draper Laboratory | 2017, November 10 – 14 | – |
| Jiří Vyskočil | Czech Technical University in Prague | 2017, October 2 – 31 | Strong Modular Proof Assistance |
| Chad Brown | Czech Technical University in Prague | 2017, October 2 – 31 | Strong Modular Proof Assistance |
| Makarius Wenzel | Sketis.net | 2017, September 11 – 13 | Certification Redux |
| Masahiko Sakai | Nagoya University | 2017, August 29 – 30 | – |
| Nao Hirokawa | JAIST | 2017, August 8 – 16 | Confluence to UNF |
| Jose Divasón | Universidad de La Rioja | 2017, June 1 – 15 | Certifying Termination and Complexity |
| John Harrison | Intel Corporation | 2017, March 23-25 | HOL(y)Hammer |
| Karol Pąk | University of Białystok | 2016, September 30 – October 8 | Isabelle/Mizar |
| Takahito Aoto | Niigata University | 2016, September 12 – 16 | Confluence to UNF |
| Masahiko Sakai | Nagoya University | 2016, September 12 – 13 | – |
| Peter Schuster | University of Verona | 2016, March 3 | Complexity (ACAT) |
| Jose Divasón | Universidad de La Rioja | 2016, February 15 – May 15 | Certifying Termination and Complexity |
| Claudio Sacerdoti Coen | University of Bologna | 2016, January 11 – 15 | HOL(y)Hammer |
| Florian Rabe | Jacobs University Bremen | 2016, January 11 – 15 | HOL(y)Hammer |
| Marc Brockschmidt | Microsoft Research | 2015, November 4 – 6 | Certifying Termination and Complexity |
| Jordan Thayer | Charles Stark Draper Laboratory | 2015, October 29 – November 4 | – |
| Cody Roux | Charles Stark Draper Laboratory | 2015, October 29 – November 4 | – |
| David Aspinall | University of Edinburgh | 2015, August 25 – September 4 | HOL(y)Hammer |
| Federico Aschieri | TU Wien | 2015, June 1 – 5 | Complexity (ACAT) |
| Jose Divasón | Universidad de La Rioja | 2015, May 19 – 22 | Certifying Termination and Complexity |
| Florian Haftmann | TU Munich | 2015, January 27 – 28 | – |
| Akihisa Yamada | Nagoya University | 2014, September 12 | – |
| Jasmin Blanchette | TU Munich | 2014, June 23 – 27 | HOL(y)Hammer |
| Josef Urban | Radboud University Nijmegen | 2014, June 13 – 21 | HOL(y)Hammer |
| Christoph Benzmuller | Freie Universität Berlin | 2014, May 22 – 23 | HOL(y)Hammer |
| Thomas Powell | Institut des Hautes Études Scientifiques | 2014, May 12 – 31 | Complexity (ACAT) |
| Nao Hirokawa | JAIST | 2014, March 24 – 28 | Constrained Rewriting and SMT |
| Hidetomo Nabeshima | University of Yamanashi | 2014, March 24 – 28 | Constrained Rewriting and SMT |
| Masahiko Sakai | Nagoya University | 2014, March 24 – 28 | Constrained Rewriting and SMT |
| Florian Rabe | Jacobs University Bremen | 2014, February 24 – 28 | HOL(y)Hammer |
| Vincent van Oostrom | Utrecht University | 2014, February 10 – 14 | Confluence |
| Karl Gmeiner | TU Wien | 2013, December 18 | Constrained Rewriting and SMT |
| Naoki Nishida | Nagoya University | 2013, December 15 – 23 | Constrained Rewriting and SMT |
| Haruhiko Sato | Hokkaido University | 2013, December 2 – 6 | Constrained Rewriting and SMT |
| Josef Urban | Radboud University Nijmegen | 2013, July 6 – 13 | – |
| Jiaxiang Liu | École Polytechnique France | 2013, April 23 – May 14 | Confluence |
The list is sorted in reverse chronological order. Only visitors from 2013 onwards are displayed.