CoChat
Sign Up
Cited by 1Logic, programming, and type systemsFormal Methods in VerificationSoftware Testing and Debugging Techniques

InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference

Open access
Li, Senxi, Yamazaki, Tetsuro, Chiba, Shigeru·2024·Schloss Dagstuhl – Leibniz-Zentrum für Informatik
DOI 10.4230/lipics.ecoop.2024.23
Open this paper in CoChat — free accountOpen PDF

Abstract

Supporting automatic type inference is in demand in modern language development. It is a challenging task but without appropriate supporting toolkits. This paper presents InferType, a Java library that helps implement constraint-based type inference. A compiler writer uses InferType’s classes and methods to describe type constraints and typing rules for type inference. InferType then performs constraint solving by translation to the Z3 SMT solver. InferType is equipped with our developed optimization technique. It reduces the search space for type variables by pre-computing the structures of those type variables for mitigating the performance bottleneck of constraint solving with deeply nested types. We use InferType to implement type inference for a subset of Python, and conduct experiments to evaluate how the developed optimization technique can affect the performance of type inference. Our results show that InferType’s optimization can greatly mitigate the performance bottleneck for programs with deeply nested types, and can potentially improve the performance for large nested types.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.4230/lipics.ecoop.2024.23

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • File-level benchmarks including CodeNet, Avatar, CodeScope, and CodeTransOcean evaluate translation of a complete program file.

    “File-level code translation benchmarks which include CodeNet [37], Avatar [38], CodeScope [39] and CodeTransOcean [40] refer to evaluating the translation of a complete program file.”

    From RepoTransBench: A Real-World Multilingual Benchmark for Repository-Level Code Translation (2026) · cites this paper as [37]

    The ‘Further Uses of CodeNet’ section (p. 19) says CodeNet may be used for program translation, supporting its inclusion as a translation dataset. The passages do not establish that it evaluates translation of a complete program file, or describe Avatar, CodeScope, and CodeTransOcean as file-level benchmarks. (LLM, conf=0.78)

    Experimental — accuracy not yet measured

  • Real repositories typically contain existing test suites that can serve as validation mechanisms.

    “Furthermore, unlike artificially crafted datasets used in fine-grained translation [37], [38], real repositories typically contain existing test suites that can serve as valuable validation mechanisms.”

    From RepoTransBench: A Real-World Multilingual Benchmark for Repository-Level Code Translation (2026) · cites this paper as [37]

    The indexed passages discuss CodeNet datasets and online-judge acceptance metadata (Sections 5.1 and 9, pp. 6 and 19), not test suites in real repositories. Searches for existing test suites, repository validation, and test cases as correctness oracles found no passage supporting the attributed claim. (LLM, conf=0.74)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

No references could be resolved yet.

Research works printed but not linked: 35

  1. [1][1] Miltiadis Allamanis, Earl T Barr, Premkumar Devanbu, and Charles Sutton. A survey of machine learning for big code and naturalness. ACM Computing Surveys (CSUR) , 51(4):1-37, 2018. -
  2. [2][2] Yanming Yang, Xin Xia, David Lo, and John Grundy. A survey on deep learning for software engineering. arXiv preprint arXiv:2011.14597 , 2020. - · arXiv
  3. [3][3] Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, Mohammad Bavarian, Clemens Winter, Philippe Tillet, Felipe Petroski Such, Dave Cummings, Matthias Plappert, Fotios Chantzis, Elizabeth Barnes, Ariel Herbert-Voss, William Hebgen Guss, Alex Nichol, Alex Paino, Nikolas Tezak, Jie Tang, Igor Babuschkin, Suchir Balaji, Shantanu Jain, William Saunders, Christopher Hesse, Andrew N. Carr, Jan Leike, Josh Achiam, Vedant Misra, Evan Morikawa, Alec Radford, Matthew Knight, Miles Brundage, Mira Murati, Katie Mayer, Peter Welinder, Bob McGrew, Dario Amodei, Sam McCandlish, Ilya Sutskever, and Wojciech Zaremba. Evaluating large language models trained on code, 2021. -
  4. [4][4] Marie-Anne Lachaux, Baptiste Roziere, Lowik Chanussot, and Guillaume Lample. Unsupervised translation of programming languages. In NeurIPS , 2020. -
  5. [5][5] Zheng Wang and Michael O'Boyle. Machine learning in compiler optimization. Proceedings of the IEEE , 106(11):1879-1901, 2018. -
  6. [10][10] Yunhui Zheng, Saurabh Pujar, Burn Lewis, Luca Buratti, Edward Epstein, Bo Yang, Jim Laredo, Alessandro Morari, and Zhong Su. D2a: A dataset built for ai-based vulnerability detection methods using differential analysis. In Proceedings of the ACM/IEEE 43rd International Conference on Software Engineering: Software Engineering in Practice , ICSE-SEIP '21, New York, NY, USA, 2021. Association for Computing Machinery. -
  7. [11][11] Yaqin Zhou, Shangqing Liu, Jingkai Siow, Xiaoning Du, and Yang Liu. Devign: Effective vulnerability identification by learning comprehensive programsemantics via graph neural networks. In Advances in Neural Information Processing Systems , pages 10197-10207. NeurIPS Foundation, 2019. -
  8. [12][12] Zhangyin Feng, Daya Guo, Duyu Tang, Nan Duan, Xiaocheng Feng, Ming Gonga, Linjun Shou, Bing Qin, Ting Liu, and Daxin Jiang. Codebert: A pre-trained model for programming and natural languages. arXiv preprint arXiv:2002.08155v4 , 2020. - · arXiv
  9. [13][13] Miltiadis Allamanis and Charles Sutton. Mining source code repositories at massive scale using language modeling. In 10th Working Conference on Mining Software Repositories (MSR) , page 207-216. IEEE, 2013. -
  10. [14][14] Veselin Raychev, Pavol Bielik, and Martin Vechev. Probabilistic model for code with decision trees. ACM SIGPLAN Notices , 2016. -
  11. [15][15] Michele Tufano, Cody Watson, Gabriele Bavota, Massimiliano Di Penta, Martin White, and Denys Poshyvanyk. An empirical study on learning bug-fixing patches in the wild via neural machine translation. In ACMTransactions on Software Engineering and Methodology (TOSEM) , pages 1-29, 2019. -
  12. [16][16] Hamel Husain, Ho-Hsiang Wu, Tiferet Gazit, Miltiadis Allamanis, and Marc Brockschmidt. Codesearchnet challenge: Evaluating the state of semantic code search. arXiv preprint arXiv:1909.09436v3 , 2019. - · arXiv
  13. [17][17] Srinivasan Iyer, Ioannis Konstas, Alvin Cheung, and Luke Zettlemoyer. Mapping language to code in programmatic context. arXiv preprint arXiv:1808.09588 , 2018. - · arXiv
  14. [19][19] Tal Ben-Nun, Alice Shoshana Jakobovits, and Torsten Hoefler. Neural code comprehension: A learnable representation of code semantics. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems 31 , pages 3588-3600. Curran Associates, Inc., 2018. -
  15. [20][20] Farhan Ullah, Hamad Naeem, Sohail Jabbar, Shehzad Khalid, Muhammad Ahsan Latif, Fadi Al-turjman, and Leonardo Mostarda. Cyber security threats detection in internet of things using deep learning approach. IEEE Access , 7:124379-124389, 2019. -
  16. [23][23] gcj-dataset. https://openreview.net/attachment?id=AZ4vmLoJft&name= supplementary\_material . -
  17. [24][24] Miltiadis Allamanis. The adverse effects of code duplication in machine learning models of code. In Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software , Onward! 2019, page 143-153, New York, NY, USA, 2019. Association for Computing Machinery. -
  18. [26][26] Terence Parr. The Definitive ANTLR 4 Reference . Pragmatic Bookshelf, 2nd edition, 2013. -
  19. [27][27] Sifei Luan, Di Yang, Celeste Barnaby, Koushik Sen, and Satish Chandra. Aroma: code recommendation via structural code search. Proceedings of the ACM on Programming Languages , 3(OOPSLA):1-28, Oct 2019. -
  20. [34][34] Thomas N. Kipf and Max Welling. Semi-supervised classification with graph convolutional networks. In ICLR , 2017. -
  21. [35][35] Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? In ICLR , 2019. -
  22. [36][36] Veronika Thost and Jie Chen. Directed acyclic graph neural networks. In ICLR , 2021. -
  23. [37][37] Shuai Lu, Daya Guo, Shuo Ren, Junjie Huang, Alexey Svyatkovskiy, Ambrosio Blanco, Colin B. Clement, Dawn Drain, Daxin Jiang, Duyu Tang, Ge Li, Lidong Zhou, Linjun Shou, Long Zhou, Michele Tufano, Ming Gong, Ming Zhou, Nan Duan, Neel Sundaresan, Shao Kun Deng, Shengyu Fu, and Shujie Liu. Codexglue: A machine learning benchmark dataset for code understanding and generation. CoRR , abs/2102.04664, 2021. - · arXiv
  24. [39][39] Weihua Hu, Matthias Fey, Marinka Zitnik, Yuxiao Dong, Hongyu Ren, Bowen Liu, Michele Catasta, and Jure Leskovec. Open graph benchmark: Datasets for machine learning on graphs. arXiv preprint arXiv:2005.00687 , 2020. - · arXiv
  25. [40][40] Matthias Fey and Jan E. Lenssen. Fast graph representation learning with PyTorch Geometric. In ICLR Workshop on Representation Learning on Graphs and Manifolds , 2019. -
  26. [41][41] Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, highperformance deep learning library. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'AlchéBuc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems 32 , pages 8024-8035. Curran Associates, Inc., 2019. -
  27. [43][43] Hitesh Sajnani. Large-Scale Code Clone Detection . PhD thesis, University of California, Irvine, 2016. -
  28. [44][44] Yujia Li, Chenjie Gu, Thomas Dullien, Oriol Vinyals, and Pushmeet Kohli. Graph matching network for learning the similarity of graph structured objects. In International Conference on Machine Learning (ICML) , 2019. -
  29. [46][46] Kevin Musgrave, Serge J. Belongie, and Ser-Nam Lim. A metric learning reality check. CoRR , abs/2003.08505, 2020. - · arXiv
  30. [49][49] Zimin Chen, Steve Kommrusch, Michele Tufano, Louis-Noël Pouchet, Denys Poshyvanyk, and Martin Monperrus. Sequencer: Sequence-to-sequence learning for end-to-end program repair. IEEE Transaction on Software Engineering , 2019. -
  31. [50][50] Michihiro Yasunaga and Percy Liang. Break-it-fix-it: Unsupervised learning for program repair. In International Conference on Machine Learning (ICML) , 2021. -
  32. [51][51] Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoc V. Le, Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, Jeff Klingner, Apurva Shah, Melvin Johnson, Xiaobing Liu, Łukasz Kaiser, Stephan Gouws, Yoshikiyo Kato, Taku Kudo, Hideto Kazawa, Keith Stevens, George Kurian, Nishant Patil, Wei Wang, Cliff Young, Jason Smith, Jason Riesa, Alex Rudnick, Oriol Vinyals, Greg Corrado, Macduff Hughes, and Jeffrey Dean. Google's neural machine translation system: Bridging the gap between human and machine translation. Preprint arXiv:1609.08144, 2016. - · arXiv
  33. [52][52] Xinyun Chen, Chang Liu, and Dawn Song. Tree-to-tree neural networks for program translation. In NeurIPS , 2018. -
  34. [53][53] Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc'Aurelio Ranzato. Unsupervised machine translation using monolingual corpora only. In ICLR , 2018. -
  35. [54][54] Shuai Lu, Daya Guo, Shuo Ren, Junjie Huang, Alexey Svyatkovskiy, Ambrosio Blanco, Colin Clement, Dawn Drain, Daxin Jiang, Duyu Tang, Ge Li, Lidong Zhou, Linjun Shou, Long Zhou, Michele Tufano, Ming Gong, Ming Zhou, Nan Duan, Neel Sundaresan, Shao Kun Deng, Shengyu Fu, and Shujie Liu. CodeXGLUE: A machine learning benchmark dataset for code understanding and generation. Preprint arXiv:2102.04664, 2021. · arXiv

Cited by

Sorted by citations

Authors
Li, S., Yamazaki, T., & Chiba, S.
Affiliations
The University of Tokyo (JP)
ORCID
Venue
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Publisher
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Published
2024
DOI
10.4230/lipics.ecoop.2024.23
OpenAlex
W7223746129
Cited by
0
References
0
FWCI
0.00
Type
journal article
Language
en
Open access
Licence
Locations
  • DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) (submittedVersion, cc-by)
  • Leibniz international proceedings in informatics (cc-by)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
Keywords
constraint-based type inference, Z3 SMT solver, typing rules, type constraints

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review