Travelled to:1 × Taiwan
1 × USA
2 × Germany
Collaborated with:J.Urban C.Urban D.A.0001 M.F.0002 S.Schulz J.Vyskocil C.E.Brown T.Gauthier G.Sutcliffe
Talks about:proof (3) isabell (2) hol (2) reconstruct (1) quotient (1) descript (1) challeng (1) tableau (1) revisit (1) general (1)
Person: Cezary Kaliszyk
DBLP: Kaliszyk:Cezary
Contributed to:
20152013
2011
2011
201620172019Wrote 7 papers:
- CADE-2015-KaliszykSUV
- System Description: E.T. 0.1 (CK, SS, JU, JV), pp. 389–398.
- CADE-2013-KaliszykU #named #proving #re-engineering
- PRocH: Proof Reconstruction for HOL Light (CK, JU), pp. 267–274.
- ESOP-2011-UrbanK
- General Bindings and α-Equivalence in Nominal Isabelle (CU, CK), pp. 480–500.
- SAC-2011-KaliszykU #higher-order
- Quotients revisited for Isabelle/HOL (CK, CU), pp. 1639–1644.
- FASE-2016-0001K #metric #proving #towards
- Towards Formal Proof Metrics (DA0, CK), pp. 325–341.
- CADE-2017-FarberKU #monte carlo #proving
- Monte Carlo Tableau Proof Search (MF0, CK, JU), pp. 563–579.
- CADE-2019-BrownGKSU #challenge #named
- GRUNGE: A Grand Unified ATP Challenge (CEB, TG, CK, GS, JU), pp. 123–141.