Coinductive Soundness of Corecursive Type Class Resolution. - Frantisek Farka; Ekaterina Komendantskaya; Kevin Hammond (LOPSTR, 2016)

Coinductive Soundness of Corecursive Type Class Resolution. - Frantisek Farka; Ekaterina Komendantskaya; Kevin Hammond; Peng Fu 001 (CoRR, 2016)

CoALP-Ty'16. - Ekaterina Komendantskaya; Frantisek Farka (CoRR, 2016)

Proof-Relevant Resolution for Elaboration of Programming Languages. - Frantisek Farka (ICLP (Technical Communications), 2018)

Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis. - Frantisek Farka; Ekaterina Komendantskaya; Kevin Hammond (Theory Pract. Log. Program., 2018)

Proof-Carrying Plans. - Christopher Schwaab; Ekaterina Komendantskaya; Alasdair Hill; Frantisek Farka; Ronald P. A. Petrick; Joe B. Wells; Kevin Hammond (PADL, 2019)

slepice: Towards a Verified Implementation of Type Theory in Type Theory. - Frantisek Farka (LOPSTR, 2020)

On algebraic abstractions for concurrent separation logics. - Frantisek Farka; Aleksandar Nanevski; Anindya Banerjee 001; Germán Andrés Delbianco; Ignacio Fábregas (Proc. ACM Program. Lang., 2021)

Developing With Formal Methods at BedRock Systems, Inc. - Gregory Malecha; Gordon Stewart 001; Frantisek Farka; Jasper Haag; Yoichi Hirai (IEEE Secur. Priv., 2022)