Skip to main content

Yutaka Nagashima

Yutaka Nagashima
Research Assistant

Research Interests

Yutaka's research interests include proof assistants and proof automation.

Contact Details

Email:Yutaka.Nagashima@data61.csiro.au
Web:https://github.com/data61/PSL

More contact information is available at the Contact page.

Publication List


Yutaka is working on the development a proof strategy language called PSL.

Projects

Past

The development of a proof strategy language (PSL).

Publications

Data61 Papers

2016

Abstract PDF Yutaka Nagashima and Liam O'Connor
Close encounters of the higher kind - emulating constructor classes in standard ML
Abstract, ACM SIGPLAN Workshop on ML, September, 2016.
Abstract PDF Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein
Refinement through restraint: Bringing down the cost of verification
International Conference on Functional Programming, Nara, Japan, September, 2016
Abstract PDF Yutaka Nagashima
Keep failed proof attempts in memory
Isabelle Workshop 2016, Nancy, France, August, 2016
Abstract PDF Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein
A framework for the automatic formal verification of refinement from Cogent to C
International Conference on Interactive Theorem Proving, Nancy, France, August, 2016

NICTA Papers

2016

Abstract PDF Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein and Gernot Heiser
Cogent: verifying high-assurance file system implementations
International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 175-188, Atlanta, GA, USA, April, 2016

Non-NICTA Papers

2016

Abstract PDF Yutaka Nagashima and Liam O'Connor
Close encounters of the higher kind - emulating constructor classes in standard ML
Abstract, ACM SIGPLAN Workshop on ML, September, 2016.
Abstract PDF Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein
Refinement through restraint: Bringing down the cost of verification
International Conference on Functional Programming, Nara, Japan, September, 2016
Abstract PDF Yutaka Nagashima
Keep failed proof attempts in memory
Isabelle Workshop 2016, Nancy, France, August, 2016
Abstract PDF Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein
A framework for the automatic formal verification of refinement from Cogent to C
International Conference on Interactive Theorem Proving, Nancy, France, August, 2016