Checking type safety of foreign function calls

Michael Furr, Jeffrey S. Foster
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]
Read: 14 June 2021

Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation
PLDI '05
Chicago, IL, USA
Association for Computing Machinery
New York, NY, USA
Pages 62-72
2005
Note(s): foreign function interface, dependent type, type inference
Papers: condit:esop:2007

Checks foreign function interface calls between O’Caml and C. The important code (i.e., where the bugs happen) is the C code. They use a flow-sensitive type system based on the data representation to detect shape errors and they use an effect system to detect when calls from C to O’Caml (that could cause a GC) are made without appropriate precautions.