小林 直樹

On the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic 

Lecture Notes in Computer Science 402-428 2025年5月1日  査読有り

Towards neural-network-guided program synthesis and verification 

Formal Methods in System Design 2025年2月24日  査読有り筆頭著者責任著者

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus 

Proceedings of the ACM on Programming Languages 9(POPL) 1136-1166 2025年1月7日  査読有り筆頭著者責任著者

Asynchronous unfold/fold transformation for fixpoint logic. 

Sci. Comput. Program. 231 103014-103014 2024年1月  査読有り

Higher-Order Property-Directed Reachability. 

Proceedings of the ACM on Programming Languages 7(ICFP) 48-77 2023年8月  査読有り

HFL(Z) Validity Checking for Automated Program Verification. 

Proc. ACM Program. Lang. 7(POPL) 154-184 2023年1月  査読有り筆頭著者責任著者

RustHorn: CHC-based Verification for Rust Programs. 

ACM Transactions on Programming Languages and Systems 43(4) 15-54 2021年  査読有り

Temporal Verification of Programs via First-Order Fixpoint Logic 

Proceedings of SAS 2019, Springer LNCS 11822 2019年10月  査読有り筆頭著者責任著者

10 Years of the Higher-Order Model Checking Project (Extended Abstract) 

Proceedings of PPDP 2019 2:1-2:2 2019年10月  招待有り

On the Termination Problem for Probabilistic Higher-Order Recursive Programs 

Proceedings of LICS 2019 1-15 2019年6月  査読有り筆頭著者責任著者

Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence 

Logical Methods in Computer Science 15(1) 53-68 2019年2月  査読有り

Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable 

Theor. Comput. Sci. 777 409-416 2019年  査読有り

Higher-order program verification via HFL model checking 

Proceedings of ESOP 2018, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 10801 711-738 2018年  査読有り筆頭著者責任著者

Pumping lemma for higher-order languages 

Proceedings of ICALP 2017, Leibniz International Proceedings in Informatics, LIPIcs 80 97:1 2017年7月1日  査読有り

Deadlock analysis of unbounded process networks 

INFORMATION AND COMPUTATION 252 48-70 2017年2月  査読有り筆頭著者責任著者

On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic 

Proceedings of POPL 2017, ACM SIGPLAN NOTICES 52(1) 246-259 2017年1月  査読有り筆頭著者責任著者

Almost Every Simply Typed \(λ\)-Term Has a Long \(β\)-Reduction Sequence 

Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, 10203 53-68 2017年  査読有り

Temporal verification of higher-order functional programs 

Conference Record of the Annual ACM Symposium on Principles of Programming Languages 57-68 2016年1月11日  査読有り

Predicate abstraction and CEGAR for disproving termination of Higher-Order functional programs 

Proceedings of CAV 2015, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 9207 287-303 2015年  査読有り

Unsafe order-2 tree languages are context-sensitive 

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 8412 149-163 2014年  査読有り筆頭著者責任著者

Model Checking Higher-Order Programs 

JOURNAL OF THE ACM 60(3) 20:1 2013年6月  査読有り

Towards a scalable software model checker for higher-order programs 

PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013 53-62 2013年  査読有り

Pumping by Typing 

2013 28TH ANNUAL IEEE/ACM SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) 398-407 2013年  査読有り

Automating Relatively Complete Verification of Higher-Order Functional Programs 

ACM SIGPLAN NOTICES 48(1) 75-86 2013年1月  査読有り

Functional programs as compressed data 

Higher-Order and Symbolic Computation 25(1) 39-84 2012年3月1日  査読有り筆頭著者責任著者

Predicate Abstraction and CEGAR for Higher-Order Model Checking 

ACM SIGPLAN NOTICES 46(6) 222-233 2011年6月  査読有り筆頭著者責任著者

COMPLEXITY OF MODEL CHECKING RECURSION SCHEMES FOR FRAGMENTS OF THE MODAL MU-CALCULUS 

LOGICAL METHODS IN COMPUTER SCIENCE 7(4) 223 2011年  査読有り筆頭著者責任著者

Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols 

AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS 6996 75-+ 2011年  査読有り

Predicate Abstraction and CEGAR for Higher-Order Model Checking 

PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION 222-233 2011年  査読有り筆頭著者責任著者

Environmental Bisimulations for Higher-Order Languages 

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 33(1) 5:1 2011年1月  査読有り

A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes 

24TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS 179-+ 2009年  査読有り筆頭著者責任著者

Dependent Type Inference with Interpolants 

PPDP'09: PROCEEDINGS OF THE 11TH INTERNATIONAL ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING 277-288 2009年  査読有り

Linear declassification 

PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS 4960 224-238 2008年  査読有り

A new type system for deadlock-free processes 

CONCUR 2006 - CONCURRENCY THEORY, PROCEEDINGS 4137 233-247 2006年  査読有り

Type-based information flow analysis for the pi-calculus 

ACTA INFORMATICA 42(4-5) 291-347 2005年12月  査読有り

Resource usage analysis 

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 27(2) 264-313 2005年3月  査読有り

A generic type system for the Pi-calculus 

THEORETICAL COMPUTER SCIENCE 311(1-3) 121-163 2004年1月  査読有り

Type systems for concurrent programs 

FORMAL METHODS AT THE CROSSROADS: FROM PANACEA TO FOUNDATIONAL SUPPORT 2757 439-453 2003年  査読有り

A type system for lock-free processes 

INFORMATION AND COMPUTATION 177(2) 122-159 2002年9月  査読有り

Type-based useless-variable elimination 

Higher-Order and Symbolic Computation 14(2-3) 221-260 2001年9月  査読有り

Type reconstruction for linear pi-calculus with I/O subtyping 

INFORMATION AND COMPUTATION 161(1) 1-44 2000年8月  査読有り

Linearity and the pi-calculus 

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 21(5) 914-947 1999年9月  査読有り筆頭著者責任著者

Quasi-Linear Types 

POPL '99, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999 29-42 1999年  査読有り

A partially deadlock-free typed process calculus 

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS 20(2) 436-482 1998年3月  査読有り