4 papers
Polymorphic Higher-order Termination
Łukasz Czajka, Cynthia Kop
We generalise the termination method of higher-order polynomial interpretations to a setting with impredicative polymorphism. Instead of using weakly monotonic functionals, we inte…
Concrete Semantics with Coq and CoqHammer
Łukasz Czajka, Burak Ekici, Cezary Kaliszyk
The "Concrete Semantics" book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of…
Goal Translation for a Hammer for Coq (Extended Abstract)
Łukasz Czajka, Cezary Kaliszyk
Hammers are tools that provide general purpose automation for formal proof assistants. Despite the gaining popularity of the more advanced versions of type theory, there are no ham…
Partiality and Recursion in Higher-order Logic
Łukasz Czajka
We present an illative system I_s of classical higher-order logic with subtyping and basic inductive types. The system I_s allows for direct definitions of partial and general recu…