Using a Generalisation Critic to find Bisimulations for Coinductive Proofs

QR Code

Using a Generalisation Critic to find Bisimulations for Coinductive Proofs

Coinduction is a method of growing importance in reasoning about functional languages, due to the increasing prominence of lazy data structures. Through the use of bisimulations and proofs that bisimilarity is a congruence in various domains it can be used to prove the congruence of two processes....

Full description

Bibliographic Details
Main Authors:	Dennis, Louise Abigail, Bundy, Alan, Green, Ian
Other Authors:	McCune, William
Format:	Conference or Workshop Item
Published:	Springer 1999
Online Access:	https://eprints.nottingham.ac.uk/344/

Similar Items

The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction
by: Dennis, Louise Abigail, et al.
Published: (2000)

A Comparison of two Proof Critics: Power vs. Robustness
by: Dennis, Louise Abigail, et al.
Published: (2002)

The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs
by: Dennis, Louise Abigail
Published: (2004)

An Architecture for Proof Planning Systems
by: Dennis, Louise Abigail
Published: (2005)

The coinductive formulation of common knowledge
by: Baston, Colm, et al.
Published: (2018)

What can be learned from failed proofs of non-theorems?
by: Dennis, Louise Abigail, et al.
Published: (2005)

On the comparison of proof planning systems: Lambda-clam, Omega and IsaPlanner
by: Dennis, Louise Abigail, et al.
Published: (2005)

Using coalgebra and coinduction to define ontology-based multi-agent systems
by: Hadzic, Maja, et al.
Published: (2008)

Findings in genome-wide association studies on asthma lack generalisation
by: Zhang, Guicheng, et al.
Published: (2010)

Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain
by: Dennis, Louise Abigail, et al.
Published: (2001)

Avoiding the Problem: A study on the generalisation of avoidance behaviour
by: Fisher, Courteney Tiegan Louise
Published: (2025)

Convergence Proof of Some Generalised Backward Differentiation (GBDF) Methods to Solve the General Second Order Ordinary Differential Equations (ODE).
by: Suleiman, Mohamed
Published: (1984)

Integrating SVC and HOL with the PROSPER Toolkit
by: Stevenson, Alan, et al.
Published: (2000)

Burdens of proof and the case for unevenness
by: Aijaz, Imran, et al.
Published: (2013)

Evaluating risk in precious metal prices with generalised lambda, generalised pareto and generalised extreme value distributions
by: Chinhamu, K., et al.
Published: (2017)

Student attitudes to plagiarism and collusion within computer science
by: Dennis, Louise Abigail
Published: (2005)

Generalised Taylor and Generalised Calvo Price and Wage Setting: Micro-evidence with Macro Implications
by: Dixon, H., et al.
Published: (2012)

Generalised fleet maintenance modelling
by: Reyes Campaña, Héctor Rodrigo
Published: (2019)

Interactive proof systems
by: Makarin, Rusydi Hasan, et al.
Published: (2011)

Zero-knowledge-proof
by: Alshaikhli, Imad Fakhri Taha, et al.
Published: (2011)

Error Proofing In Manufacturing.
by: Nadarajah, Sivakumar
Published: (2006)

Error Proofing In Manufacturing
by: Nadarajah, Sivakumar
Published: (2006)

Error Proofing In Manufacturing
by: Nadarajah, Sivakumar
Published: (2006)

Rule Generalisation in Intrusion Detection Systems using Snort
by: Aickelin, Uwe, et al.
Published: (2007)

Rule Generalisation in Intrusion Detection Systems using Snort
by: Aickelin, Uwe, et al.
Published: (2007)

Generalised relative defects of meromorphic function
by: Indrajit Lahiri ,, et al.
Published: (1996)

Generalisation of close-to-convex of complex order
by: Khalida Inayat Noor,, et al.
Published: (2010)

Generalisation of scattering theory to charged particles
by: Kadyrov, Alisher, et al.
Published: (2009)

Generalisation of n-centraliser rings and their graphs
by: Chan, Tai Chong
Published: (2024)

Generalised lambert function and its applications
by: Chew, Chun Yong
Published: (2024)

Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus
by: Zimmer, Juergen, et al.
Published: (2002)

The NumbersWithNames Program
by: Colton, Simon, et al.
Published: (2002)

System Description: Embedding Verification into Microsoft Excel
by: Collins, Graham, et al.
Published: (2000)

Datatype-generic termination proofs
by: Backhouse, Roland, et al.
Published: (2008)

Proof Methods for Corecursive Programs
by: Hutton, Graham, et al.
Published: (2005)

Background of zero-knowledge proof
by: Alshaikhli, Imad Fakhri Taha, et al.
Published: (2011)

No proof vaccine linked to deaths
by: Krishnan, Dhesegaran Bala
Published: (2021)

Aspects of galileons and generalised scalar-tensor theories
by: Sivanesan, Vishagan
Published: (2014)

Generalised impossible differentials of advanced encryption standard
by: Phan, R.C.W., et al.
Published: (2001)

Unified notions of generalised monads and applicative functors
by: Bracker, Jan
Published: (2018)