F5 Toolchain for RCF

F5 is a toolchain for Refined Concurrent FPC (RCF) including a type-checker with union, intersection, and polymorphic types, as well as static reasoning about type disjointness, and a user-friendly GUI for examining typing derivations; an automatic code generator for symbolic implementations of zero-knowledge; a visual debugger, and more.



Download Coq formalization of our calculus, type system and soundness proof by Cătălin Hriţcu. Works with Coq 8.2.


Download F5 tool-chain for RCF by Thorsten Tarrach and Cătălin Hriţcu  Apache License, Version 2.0.


Bug Tracker

Because of a recent spam wave you need to be logged-in to create new tickets. If you need an account or want to report a bug directly please contact catalin.hritcu@….