BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × Canada
1 × Cyprus
1 × Greece
1 × Hungary
1 × India
1 × Spain
13 × USA
2 × Poland
2 × Portugal
3 × France
4 × Italy
4 × Japan
4 × United Kingdom
Collaborated with:
H.Unno ∅ A.Igarashi T.Tsukada A.Yonezawa R.Sato K.Suenaga C.L.Ong D.Sangiorgi E.Sumii F.Iwama T.Terauchi T.Kuwahara X.Li C.H.Broadbent D.Kikuchi Y.Kaneko H.Ohsaki T.Suto K.Asada K.Inaba Y.Tobita K.Matsuda A.Shinohara N.Tabuchi L.Wischik B.C.Pierce D.N.Turner M.Nakade
Talks about:
type (18) program (16) order (16) higher (14) model (10) check (9) analysi (8) function (7) calculus (7) recurs (7)

Person: Naoki Kobayashi

DBLP DBLP: Kobayashi_0001:Naoki

Facilitated 3 volumes:

ICALP (1) 2015Ed
ICALP (2) 2015Ed
FLOPS 2010Ed

Contributed to:

CAV 20152015
LICS 20152015
PEPM 20152015
ESOP 20142014
FoSSaCS 20142014
CSL 20132013
ESOP 20132013
PEPM 20132013
POPL 20132013
FLOPS 20122012
PEPM 20122012
PLDI 20112011
FOSSACS 20102010
POPL 20102010
ESOP 20092009
ICALP (2) 20092009
LICS 20092009
POPL 20092009
PPDP 20092009
CAV 20082008
ESOP 20082008
FLOPS 20082008
RTA 20082008
ESOP 20072007
ICALP 20072007
LICS 20072007
PEPM 20062006
VMCAI 20062006
LOPSTR 20052005
ASIA-PEPM 20022002
POPL 20022002
POPL 20012001
PEPM 20002000
POPL 19991999
SAS 19971997
POPL 19961996
SAS 19951995
OOPSLA 19941994
ILPS 19931993

Wrote 43 papers:

CAV-2015-KuwaharaSU0 #abstraction #functional #higher-order #source code #termination
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs (TK, RS, HU, NK), pp. 287–303.
LICS-2015-KobayashiL #abstraction #model checking #refinement
Automata-Based Abstraction Refinement for μHORS Model Checking (NK, XL), pp. 713–724.
PEPM-2015-AsadaS0 #first-order #functional #refinement #relational #source code #verification
Verifying Relational Properties of Functional Programs by First-Order Refinement (KA, RS, NK), pp. 61–72.
ESOP-2014-KuwaharaTU0 #automation #functional #higher-order #source code #termination #verification
Automatic Termination Verification for Higher-Order Functional Programs (TK, TT, HU, NK), pp. 392–411.
FoSSaCS-2014-KobayashiIT #higher-order
Unsafe Order-2 Tree Languages Are Context-Sensitive (NK, KI, TT), pp. 149–163.
FoSSaCS-2014-Tsukada0 #call-by #complexity #model checking #source code
Complexity of Model-Checking Call-by-Value Programs (TT, NK), pp. 180–194.
CSL-2013-BroadbentK #higher-order #model checking #recursion
Saturation-Based Model Checking of Higher-Order Recursion Schemes (CHB, NK), pp. 129–148.
ESOP-2013-KobayashiI #higher-order #model checking #recursion #source code
Model-Checking Higher-Order Programs with Recursive Types (NK, AI), pp. 431–450.
PEPM-2013-SatoUK #higher-order #model checking #scalability #source code #towards
Towards a scalable software model checker for higher-order programs (RS, HU, NK), pp. 53–62.
POPL-2013-UnnoTK #automation #functional #higher-order #source code #verification
Automating relatively complete verification of higher-order functional programs (HU, TT, NK), pp. 75–86.
FLOPS-2012-TobitaTK #analysis #higher-order #model checking
Exact Flow Analysis by Higher-Order Model Checking (YT, TT, NK), pp. 275–289.
PEPM-2012-KobayashiMS #functional #source code
Functional programs as compressed data (NK, KM, AS), pp. 121–130.
PLDI-2011-KobayashiSU #abstraction #higher-order #model checking
Predicate abstraction and CEGAR for higher-order model checking (NK, RS, HU), pp. 222–233.
FoSSaCS-2010-TsukadaK #infinity #recursion
Untyped Recursion Schemes and Infinite Intersection Types (TT, NK), pp. 343–357.
POPL-2010-KobayashiTU #higher-order #multi #recursion #transducer #verification
Higher-order multi-parameter tree transducers and recursion schemes for program verification (NK, NT, HU), pp. 495–508.
ESOP-2009-KikuchiK #authentication #automation #encryption #protocol #type system #verification
Type-Based Automated Verification of Authenticity in Cryptographic Protocols (DK, NK), pp. 222–236.
ICALP-v2-2009-KobayashiO #calculus #complexity #model checking #recursion #μ-calculus
Complexity of Model Checking Recursion Schemes for Fragments of the Modal μ-Calculus (NK, CHLO), pp. 223–234.
LICS-2009-KobayashiO #calculus #higher-order #model checking #recursion #type system #μ-calculus
A Type System Equivalent to the Modal μ-Calculus Model Checking of Higher-Order Recursion Schemes (NK, CHLO), pp. 179–188.
POPL-2009-Kobayashi #higher-order #recursion #source code #verification
Types and higher-order recursion schemes for verification of higher-order programs (NK), pp. 416–428.
PPDP-2009-Kobayashi #higher-order #model checking
Model-checking higher-order functions (NK), pp. 25–36.
PPDP-2009-UnnoK #dependent type #type inference
Dependent type inference with interpolants (HU, NK), pp. 277–288.
CAV-2008-KobayashiS #hybrid #mobile #process #type system
A Hybrid Type System for Lock-Freedom of Mobile Processes (NK, DS), pp. 80–93.
ESOP-2008-KanekoK #classification #linear
Linear Declassification (YK, NK), pp. 224–238.
FLOPS-2008-Kobayashi #program analysis #type system
Substructural Type Systems for Program Analysis (NK), p. 14.
FLOPS-2008-UnnoK #dependent type #on-demand #refinement
On-Demand Refinement of Dependent Types (HU, NK), pp. 81–96.
RTA-2008-KobayashiO #automaton
Tree Automata for Non-linear Arithmetic (NK, HO), pp. 291–305.
ESOP-2007-SuenagaK #analysis #calculus #concurrent #type system
Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts (KS, NK), pp. 490–504.
ICALP-2007-KobayashiS #behaviour #calculus #type system
Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the π -Calculus (NK, TS), pp. 740–751.
LICS-2007-SangiorgiKS #bisimulation #higher-order
Environmental Bisimulations for Higher-Order Languages (DS, NK, ES), pp. 293–302.
PEPM-2006-IwamaIK #analysis #exception #functional #resource management
Resource usage analysis for a functional language with exceptions (FI, AI, NK), pp. 38–47.
VMCAI-2006-KobayashiSW #analysis #resource management #π-calculus
Resource Usage Analysis for the pi-Calculus (NK, KS, LW), pp. 298–312.
LOPSTR-2005-SuenagaKY #approach #automation #generative #source code #type system
Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives (KS, NK, AY), pp. 98–114.
ASIA-PEPM-2002-IwamaK #type system #virtual machine
A new type system for JVM lock primitives (FI, NK), pp. 71–82.
POPL-2002-IgarashiK #analysis #resource management
Resource usage analysis (AI, NK), pp. 331–342.
POPL-2001-IgarashiK #type system #π-calculus
A generic type system for the π-calculus (AI, NK), pp. 128–141.
PEPM-2000-Kobayashi #type system
Type-Based Useless Variable Elimination (NK), pp. 84–93.
PEPM-2000-SumiiK #approach #partial evaluation
Online-and-Offline Partial Evaluation: A Mixed Approach (ES, NK), pp. 12–21.
POPL-1999-Kobayashi
Quasi-Linear Types (NK), pp. 29–42.
SAS-1997-IgarashiK #analysis #communication #concurrent #programming language #type system
Type-Based Analysis of Communication for Concurrent Programming Languages (AI, NK), pp. 187–201.
POPL-1996-KobayashiPT #π-calculus
Linearity and the π-Calculus (NK, BCP, DNT), pp. 358–371.
SAS-1995-KobayashiNY #communication #concurrent #programming language #static analysis
Static Analysis of Communication for Asynchronous Concurrent Programming Languages (NK, MN, AY), pp. 225–242.
OOPSLA-1994-KobayashiY #concurrent #object-oriented #programming
Type-Theoretic Foundations for Concurrent Object-Oriented Programming (NK, AY), pp. 31–45.
ILPS-1993-KobayashiY #concurrent #linear #logic programming #named #paradigm
ACL — A Concurrent Linear Logic Programming Paradigm (NK, AY), pp. 279–294.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.