Tachio Terauchi

Associate Professor
Graduate School of Information Science, Nagoya University
(+81)-52-789-4242
terauchi AT is DOT nagoya-u DOT ac DOT jp

Japanese version

Bio

I am a Japan born Japanese, educated mostly in America. I have B.S. from Columbia and M.S. and Ph.D. from UC Berkeley, all in computer science. I was an assistant professor at Tohoku University from 2007 to 2011. I joined Nagoya University as an associate professor in 2011.

Teaching

Computer Software 2 (Spring 2013 - registered students only)

Classes in Japanese

Professional Activities

CSL 2013 : Program Committee
POPL 2013 : External Review Committee
APLAS 2012 : Program Committee
POPL 2012 : Program Committee
TLCA 2011 : Program Committee
ESOP 2011 : Program Committee
PLPV 2011 : Program Committee
VMCAI 2011 : Program Committee
TLDI 2011 : Program Committee
PLDI 2010 : External Review Committee
PPL 2010 (Japanese) : Program Co-Chair
PLAS 2009 : Program Committee
PPL 2009 (Japanese) : Program Committee
SAC 2009 : Program Committee
SAS 2008 : Program Committee

Publications

Automating Relatively Complete Verification of Higher-Order Functional Programs.
Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi.
POPL 2013. [pdf (Full version with proofs)]
Quantitative Information Flow as Safety and Liveness Hyperproperties.
Hirotoshi Yasuoka and Tachio Terauchi.
QAPL 2012. [pdf (Full version with proofs and fixes)]
On Bounding Problems of Quantitative Information Flow (Extended Version).
Hirotoshi Yasuoka and Tachio Terauchi.
Journal of Computer Security 19(6):2011. [pdf]
On Bounding Problems of Quantitative Information Flow.
Hirotoshi Yasuoka and Tachio Terauchi.
ESORICS 2010. [pdf (Full version with proofs)]
Quantitative Information Flow - Verification Hardness and Possibilities.
Hirotoshi Yasuoka and Tachio Terauchi.
CSF 2010. [pdf (Full version with proofs)]
Dependent Types from Counterexamples.
Tachio Terauchi.
POPL 2010. [pdf (Full version with proofs and fixes)]
Demo

Polymorphic Fractional Capabilities.
Hirotoshi Yasuoka and Tachio Terauchi.
SAS 2009.

A Type System for Observational Determinism.
Tachio Terauchi.
CSF 2008. [pdf (With bug fixes)]

Checking Race Freedom via Linear Programming.
Tachio Terauchi.
PLDI 2008. [pdf (With minor bug fixes)]

A Capability Calculus for Concurrency and Determinism (Extended Version).
Tachio Terauchi and Alex Aiken.
TOPLAS 30(5): (2008). [pdf]

Witnessing Side Effects (Extended Version).
Tachio Terauchi and Alex Aiken.
TOPLAS 30(3): (2008). [pdf]

Inferring Channel Buffer Bounds via Linear Programming.
Tachio Terauchi and Adam Megacz.
ESOP 2008. [pdf]

A Capability Calculus for Concurrency and Determinism.
Tachio Terauchi and Alex Aiken.
CONCUR 2006. [pdf (Full version with proofs)]

On Typability for Rank-2 Intersection Types with Polymorphic Recursion.
Tachio Terauchi and Alex Aiken.
LICS 2006. [pdf (Full version with proofs and fixes)]
Notes on Section 6

Witnessing Side-Effects.
Tachio Terauchi and Alex Aiken.
ICFP 2005. [pdf]
Deprecated - see the TOPLAS version.

Secure Information Flow as a Safety Problem.
Tachio Terauchi and Alex Aiken.
SAS 2005. [pdf (Full version with proofs and fixes)]

Memory Management with Use-Counted Regions.
Tachio Terauchi and Alex Aiken.
Technical Report UCB//CSD-04-1314, University of California, Berkeley, March 2004. [pdf]

Checking and Inferring Local Non-Aliasing.
Alex Aiken, Jeffrey S. Foster, John Kodumal, and Tachio Terauchi.
PLDI 2003.

Flow-Sensitive Type Qualifiers.
Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken.
PLDI 2002.

Classification of Cancer Tissue Types by Support Vector Machines Using Micro Array Gene Expression Data.
Jinsong Cai, Aynur Dayanik, Hong Yu, Naveed Hasan, Tachio Terauchi, and William N. Grundy.
ISMB 2000.

Exploring MARS: Developing Indoor and Outdoor User Interfaces to a Mobile Augmented Reality System.
Tobias Höllerer, Steven Feiner, Tachio Terauchi, Gus Rashid, and Drexel Hallaway.
Computers & Graphics 23(6): (1999).