6 citations · 15 across the 9 of their papers we have counts for
8 papers · 1 filter
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…
A new coinductive confluence proof for infinitary lambda calculus
Łukasz Czajka
We present a new and formal coinductive proof of confluence and normalisation of Böhm reduction in infinitary lambda calculus. The proof is simpler than previous proofs of this res…
An operational interpretation of coinductive types
Łukasz Czajka
We introduce an operational rewriting-based semantics for strictly positive nested higher-order (co)inductive types. The semantics takes into account the "limits" of infinite reduc…
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…
Coinduction: an elementary approach
Łukasz Czajka
The main aim of this paper is to promote a certain style of doing coinductive proofs, similar to inductive proofs as commonly done by mathematicians. For this purpose, we provide a…
Confluence of an extension of Combinatory Logic by Boolean constants
Łukasz Czajka
We show confluence of a conditional term rewriting system CL-pc, which is an extension of Combinatory Logic by Boolean constants. This solves problem 15 from the RTA list of…
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…