FORMAL VERIFICATION • TYPE SYSTEMS • CATEGORY THEORY • AUTOMATED THEOREM PROVING • PARALLEL COMPUTATION • DEPENDENT TYPES • PROOF ASSISTANTS • DISTRIBUTED SYSTEMS • MATHEMATICAL LOGIC • OPERATIONAL SEMANTICS • ABSTRACT ALGEBRA • MODAL LOGIC • FORMAL VERIFICATION • TYPE SYSTEMS • CATEGORY THEORY • AUTOMATED THEOREM PROVING • PARALLEL COMPUTATION • DEPENDENT TYPES • PROOF ASSISTANTS • DISTRIBUTED SYSTEMS • MATHEMATICAL LOGIC • OPERATIONAL SEMANTICS • ABSTRACT ALGEBRA • MODAL LOGIC • FORMAL VERIFICATION • TYPE SYSTEMS • CATEGORY THEORY • AUTOMATED THEOREM PROVING • PARALLEL COMPUTATION • DEPENDENT TYPES • PROOF ASSISTANTS • DISTRIBUTED SYSTEMS • MATHEMATICAL LOGIC • OPERATIONAL SEMANTICS • ABSTRACT ALGEBRA • MODAL LOGIC • FORMAL VERIFICATION • TYPE SYSTEMS • CATEGORY THEORY • AUTOMATED THEOREM PROVING • PARALLEL COMPUTATION • DEPENDENT TYPES • PROOF ASSISTANTS • DISTRIBUTED SYSTEMS • MATHEMATICAL LOGIC • OPERATIONAL SEMANTICS • ABSTRACT ALGEBRA • MODAL LOGIC •
FORMAL VERIFICATION • TYPE SYSTEMS • CATEGORY THEORY • AUTOMATED THEOREM PROVING • PARALLEL COMPUTATION • DEPENDENT TYPES • PROOF ASSISTANTS • DISTRIBUTED SYSTEMS • MATHEMATICAL LOGIC • OPERATIONAL SEMANTICS • ABSTRACT ALGEBRA • MODAL LOGIC • FORMAL VERIFICATION • TYPE SYSTEMS • CATEGORY THEORY • AUTOMATED THEOREM PROVING • PARALLEL COMPUTATION • DEPENDENT TYPES • PROOF ASSISTANTS • DISTRIBUTED SYSTEMS • MATHEMATICAL LOGIC • OPERATIONAL SEMANTICS • ABSTRACT ALGEBRA • MODAL LOGIC • FORMAL VERIFICATION • TYPE SYSTEMS • CATEGORY THEORY • AUTOMATED THEOREM PROVING • PARALLEL COMPUTATION • DEPENDENT TYPES • PROOF ASSISTANTS • DISTRIBUTED SYSTEMS • MATHEMATICAL LOGIC • OPERATIONAL SEMANTICS • ABSTRACT ALGEBRA • MODAL LOGIC • FORMAL VERIFICATION • TYPE SYSTEMS • CATEGORY THEORY • AUTOMATED THEOREM PROVING • PARALLEL COMPUTATION • DEPENDENT TYPES • PROOF ASSISTANTS • DISTRIBUTED SYSTEMS • MATHEMATICAL LOGIC • OPERATIONAL SEMANTICS • ABSTRACT ALGEBRA • MODAL LOGIC •
SECURE
TS//SI//TK
INTEGRITYVERIFIED
7AF2E9D1

zaph

λ

programming languages researcher

category theorist

theorem prover

current work
automated parallel computation
formal verification
type systems
research→
pl, proofs, ai
projects→
open source work
writing→
blog posts
github→
@jfulfo
SYSTEM STATUS: OPERATIONAL • UNIVERSAL PROOF ARBITER: ONLINE • ENV: PRODUCTION • BUILD: f8a2e-20240418 • SECURITY LEVEL: TS/SCI • ABSOLUTE VERIFIER: ENABLED • QUANTUM RESISTANT ENCRYPTION: ACTIVE • SYSTEM STATUS: OPERATIONAL • UNIVERSAL PROOF ARBITER: ONLINE • ENV: PRODUCTION • BUILD: f8a2e-20240418 • SECURITY LEVEL: TS/SCI • ABSOLUTE VERIFIER: ENABLED • QUANTUM RESISTANT ENCRYPTION: ACTIVE • SYSTEM STATUS: OPERATIONAL • UNIVERSAL PROOF ARBITER: ONLINE • ENV: PRODUCTION • BUILD: f8a2e-20240418 • SECURITY LEVEL: TS/SCI • ABSOLUTE VERIFIER: ENABLED • QUANTUM RESISTANT ENCRYPTION: ACTIVE • SYSTEM STATUS: OPERATIONAL • UNIVERSAL PROOF ARBITER: ONLINE • ENV: PRODUCTION • BUILD: f8a2e-20240418 • SECURITY LEVEL: TS/SCI • ABSOLUTE VERIFIER: ENABLED • QUANTUM RESISTANT ENCRYPTION: ACTIVE •
SYSTEM STATUS: OPERATIONAL • UNIVERSAL PROOF ARBITER: ONLINE • ENV: PRODUCTION • BUILD: f8a2e-20240418 • SECURITY LEVEL: TS/SCI • ABSOLUTE VERIFIER: ENABLED • QUANTUM RESISTANT ENCRYPTION: ACTIVE • SYSTEM STATUS: OPERATIONAL • UNIVERSAL PROOF ARBITER: ONLINE • ENV: PRODUCTION • BUILD: f8a2e-20240418 • SECURITY LEVEL: TS/SCI • ABSOLUTE VERIFIER: ENABLED • QUANTUM RESISTANT ENCRYPTION: ACTIVE • SYSTEM STATUS: OPERATIONAL • UNIVERSAL PROOF ARBITER: ONLINE • ENV: PRODUCTION • BUILD: f8a2e-20240418 • SECURITY LEVEL: TS/SCI • ABSOLUTE VERIFIER: ENABLED • QUANTUM RESISTANT ENCRYPTION: ACTIVE • SYSTEM STATUS: OPERATIONAL • UNIVERSAL PROOF ARBITER: ONLINE • ENV: PRODUCTION • BUILD: f8a2e-20240418 • SECURITY LEVEL: TS/SCI • ABSOLUTE VERIFIER: ENABLED • QUANTUM RESISTANT ENCRYPTION: ACTIVE •