Tachio Terauchi

Japanese version

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

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.

Professional Activities

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)

PLAS 2009 : Program Committee
PPL 2009 (Japanese) : Program Committee
SAC 2009 : Program Committee
SAS 2008 : Program Committee

Publications

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.

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): 779-785 (1999)