![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Yutaka Nagashima
Person information
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Journal Articles
- 2016
- [j3]Yutaka Nagashima:
Proof Strategy Language. Arch. Formal Proofs 2016 (2016) - 2002
- [j2]Yutaka Nagashima, Nobuyoshi Taguchi, Takakazu Ishimatsu, Hirofumi Inoue:
Development of a Compact Autonomous Underwater vehicle Using Varivec Propeller. J. Robotics Mechatronics 14(2): 112-117 (2002) - 2000
- [j1]Yutaka Nagashima, Takakazu Ishimatsu, Jamal Tariq Mian:
AUV with Variable Vector Propeller. J. Robotics Mechatronics 12(1): 60-65 (2000)
Conference and Workshop Papers
- 2023
- [c17]Yutaka Nagashima
:
Genetic Algorithm for Program Synthesis. FSEN 2023: 104-111 - [c16]Yutaka Nagashima
, Zijin Xu
, Ningli Wang
, Daniel Sebastian Goc
, James Bang
:
Template-Based Conjecturing for Automated Induction in Isabelle/HOL. FSEN 2023: 112-125 - 2022
- [c15]Kazuyuki Kaneda, Yuki Sato, Ayanari Sibayama, Kiyoshi Horie, Yutaka Nagashima:
An Underwater Environment Measuring System and Three-Dimensional Visualization of Underwater Structure Using Underwater Drone and 5G Network. GCCE 2022: 860-861 - [c14]Yutaka Nagashima
:
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction. TAP@STAF 2022: 48-66 - 2021
- [c13]Yutaka Nagashima:
Faster Smarter Proof by Induction in Isabelle/HOL. IJCAI 2021: 1981-1988 - 2020
- [c12]Yutaka Nagashima:
Smart Induction for Isabelle/HOL (Tool Paper). FMCAD 2020: 245-254 - [c11]Yutaka Nagashima
:
Simple Dataset for Proof Method Recommendation in Isabelle/HOL. CICM 2020: 297-302 - 2019
- [c10]Yutaka Nagashima
:
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL. APLAS 2019: 266-287 - [c9]Yutaka Nagashima
:
Towards evolutionary theorem proving for isabelle/HOL. GECCO (Companion) 2019: 419-420 - 2018
- [c8]Yutaka Nagashima
, Yilun He:
PaMpeR: proof method recommendation system for Isabelle/HOL. ASE 2018: 362-372 - [c7]Yutaka Nagashima
, Julian Parsert
:
Goal-Oriented Conjecturing for Isabelle/HOL. CICM 2018: 225-231 - 2017
- [c6]Yutaka Nagashima
, Ramana Kumar:
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL. CADE 2017: 528-545 - 2016
- [c5]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 C. Murray, Gerwin Klein
, Gernot Heiser:
CoGENT: Verifying High-Assurance File System Implementations. ASPLOS 2016: 175-188 - [c4]Liam O'Connor
, Zilin Chen
, Christine Rizkallah
, Sidney Amani, Japheth Lim, Toby C. Murray, Yutaka Nagashima
, Thomas Sewell, Gerwin Klein
:
Refinement through restraint: bringing down the cost of verification. ICFP 2016: 89-102 - [c3]Christine Rizkallah
, Japheth Lim, Yutaka Nagashima
, Thomas Sewell, Zilin Chen
, Liam O'Connor
, Toby C. Murray, Gabriele Keller
, Gerwin Klein
:
A Framework for the Automatic Formal Verification of Refinement from Cogent to C. ITP 2016: 323-340 - 1998
- [c2]Yutaka Nagashima, Takakazu Ishimatsu:
A Morphological Approach to Fish Discrimination. MVA 1998: 306-309 - 1996
- [c1]Yutaka Nagashima, Takeshi Nakazono, Takakazu Ishimatsu:
Parallel Implementation of Features Extraction Using Morphological Filter. MVA 1996: 426-429
Informal and Other Publications
- 2022
- [i18]Yutaka Nagashima:
Genetic Algorithm for Program Synthesis. CoRR abs/2211.11937 (2022) - [i17]Yutaka Nagashima, Zijin Xu, Ningli Wang, Daniel Sebastian Goc, James Bang:
Property-Based Conjecturing for Automated Induction in Isabelle/HOL. CoRR abs/2212.11151 (2022) - 2020
- [i16]Yutaka Nagashima:
Smart Induction for Isabelle/HOL (System Description). CoRR abs/2001.10834 (2020) - [i15]Yutaka Nagashima:
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description). CoRR abs/2004.10667 (2020) - [i14]Yutaka Nagashima:
Towards United Reasoning for Automatic Induction in Isabelle/HOL. CoRR abs/2005.12737 (2020) - [i13]Yutaka Nagashima:
Faster Smarter Induction in Isabelle/HOL with SeLFiE. CoRR abs/2009.09215 (2020) - [i12]Yutaka Nagashima:
SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL. CoRR abs/2010.10296 (2020) - 2019
- [i11]Yutaka Nagashima:
Towards Evolutionary Theorem Proving for Isabelle/HOL. CoRR abs/1904.08468 (2019) - [i10]Yutaka Nagashima:
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL. CoRR abs/1906.08084 (2019) - [i9]Yutaka Nagashima:
Designing Game of Theorems. CoRR abs/1906.08549 (2019) - [i8]Yutaka Nagashima:
Domain-Specific Language to Encode Induction Heuristics. CoRR abs/1907.02594 (2019) - 2018
- [i7]Yutaka Nagashima, Julian Parsert:
Goal-Oriented Conjecturing for Isabelle/HOL. CoRR abs/1806.04774 (2018) - [i6]Yutaka Nagashima, Yilun He:
PaMpeR: Proof Method Recommendation System for Isabelle/HOL. CoRR abs/1806.07239 (2018) - [i5]Yutaka Nagashima:
Towards Machine Learning Mathematical Induction. CoRR abs/1812.04088 (2018) - 2017
- [i4]Yutaka Nagashima:
Towards Smart Proof Search for Isabelle. CoRR abs/1701.03037 (2017) - 2016
- [i3]Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, Gerwin Klein:
COGENT: Certified Compilation for a Functional Systems Language. CoRR abs/1601.05520 (2016) - [i2]Yutaka Nagashima, Ramana Kumar:
A Proof Strategy Language and Proof Script Generation for Isabelle. CoRR abs/1606.02941 (2016) - [i1]Yutaka Nagashima, Liam O'Connor:
Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML. CoRR abs/1608.03350 (2016)
Coauthor Index
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 22:50 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint