@ARTICLE {
	AUTHOR = "Cezar-Constantin Andrici and Stefan Ciobaca and Catalin Hritcu and Guido Mart{\'{\i}}nez and Exequiel Rivas and {\'E}ric Tanter and Theo Winterhalter",
	TITLE ="Securing Verified IO Programs Against Unverified Code in F*",
	JOURNAL = "Proceedings of the ACM Programming Languages (PACMPL)",
	VOLUME = "8",
	NUMBER = "POPL",
	PAGES = "2226-2259",
	MONTH = "Jan",
	YEAR = "2024",
	PUBLISHER = "ACM Press",
	ADDRESS = "New York, NY, USA",
	ISSN ="2475-1421",
	}