![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > The Power of Parameterization in Coinductive Proof
The Power of Parameterization in Coinductive ProofAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Peter Sewell. This will be the first Semantics Lunch of the term - please do come along (or email Peter.Sewell@cl.cam.ac.uk) with offers of talks. In this talk, I will present a very simple theorem about coinduction, which we call parameterized coinduction. More precisely it is for reasoning about the greatest fixed point of a monotone function on a complete lattice. The theorem is as simple as the Knaster-Tarski fixedpoint theorem but gives a more powerful reasoning principle. I will compare our theorem with the Knaster-Tarski theorem and show its power using a simple bisimulation example. In a different point of view, the theorem captures a semantic notion of “guarded proof” in coinduction. Thus we implemented a new tactic “pcofix” replacing Coq’s primitive cofix and avoiding its syntactic guardedness checking of proof terms. You can find the Coq library at This is joint work with Georg Neis, Derek Dreyer and Viktor Vafeiadis. This talk is part of the Semantics Lunch (Computer Laboratory) series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsSchool of Clinical Medicine Talks CTSRD - CRASH-worthy Trusted Systems R&D Early Science and MedicineOther talksMaking Refuge: Academics at Risk Energy landscape of multivariate time series data TODAY Foster Talk - Integrin-associated adhesion complexes and their role in mechanotransduction Uncertainty Quantification of geochemical and mechanical compaction in layered sedimentary basins Viral evolution on sub-phylogenetic timescales THE MATHEMATICAL MAGIC OF MIXED REALITY |