A case study in programming coinductive proofs: Howe’s method (Q5236557): Difference between revisions

@@ Property / cites work @@
+Q5854733
@@ Property / cites work: Q5854733 / rank @@
+Normal rank
@@ Property / cites work @@
+Wellfounded recursion with copatterns
@@ Property / cites work: Wellfounded recursion with copatterns / rank @@
+Normal rank
@@ Property / cites work @@
+Well-founded recursion with copatterns and sized types
+Normal rank
@@ Property / cites work @@
+Copatterns
@@ Property / cites work: Copatterns / rank @@
+Normal rank
@@ Property / cites work @@
+A domain equation for bisimulation
@@ Property / cites work: A domain equation for bisimulation / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4945209
@@ Property / cites work: Q4945209 / rank @@
+Normal rank
@@ Property / cites work @@
+Abella: A System for Reasoning about Relational Specifications
+Normal rank
@@ Property / cites work @@
+Formalising the pi-calculus using nominal logic
@@ Property / cites work: Formalising the pi-calculus using nominal logic / rank @@
+Normal rank
@@ Property / cites work @@
+Psi-calculi in Isabelle
@@ Property / cites work: Psi-calculi in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Strongly typed term representations in Coq
@@ Property / cites work: Strongly typed term representations in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Foundational (co)datatypes and (co)recursion for higher-order logic
+Normal rank
@@ Property / cites work @@
+Programming with binders and indexed data-types
@@ Property / cites work: Programming with binders and indexed data-types / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing proofs with logical relations – Kripke-style
+Normal rank
@@ Property / cites work @@
+αCheck: A mechanized metatheory model checker
@@ Property / cites work: αCheck: A mechanized metatheory model checker / rank @@
+Normal rank
@@ Property / cites work @@
+Syntactic Logical Relations for Polymorphic and Recursive Types
+Normal rank
@@ Property / cites work @@
+Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
+Normal rank
@@ Property / cites work @@
+Formal foundations of operational semantics
@@ Property / cites work: Formal foundations of operational semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754137
@@ Property / cites work: Q2754137 / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Q4365103
@@ Property / cites work: Q4365103 / rank @@
+Normal rank
@@ Property / cites work @@
+\(\pi\)-calculus in (Co)inductive-type theory
@@ Property / cites work: \(\pi\)-calculus in (Co)inductive-type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Proving congruence of bisimulation in functional programming languages
+Normal rank
@@ Property / cites work @@
+Q4993349
@@ Property / cites work: Q4993349 / rank @@
+Normal rank
@@ Property / cites work @@
+Towards a mechanized metatheory of standard ML
@@ Property / cites work: Towards a mechanized metatheory of standard ML / rank @@
+Normal rank
@@ Property / cites work @@
+Equivalence in functional languages with effects
@@ Property / cites work: Equivalence in functional languages with effects / rank @@
+Normal rank
@@ Property / cites work @@
+Q4222839
@@ Property / cites work: Q4222839 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming with Higher-Order Logic
@@ Property / cites work: Programming with Higher-Order Logic / rank @@
+Normal rank
@@ Property / cites work @@
+A proof theory for generic judgments
@@ Property / cites work: A proof theory for generic judgments / rank @@
+Normal rank
@@ Property / cites work @@
+Fully abstract models of typed \(\lambda\)-calculi
+Normal rank
@@ Property / cites work @@
+Q2844810
@@ Property / cites work: Q2844810 / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Contextual modal type theory
@@ Property / cites work: Contextual modal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Higher-order psi-calculi
@@ Property / cites work: Higher-order psi-calculi / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying termination and reduction properties about higher-order logic programs
+Normal rank
@@ Property / cites work @@
+A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
+Normal rank
@@ Property / cites work @@
+An insider's look at LF type reconstruction: everything you (n)ever wanted to know
+Normal rank
@@ Property / cites work @@
+Q5277845
@@ Property / cites work: Q5277845 / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive Beluga: Programming Proofs
@@ Property / cites work: Inductive Beluga: Programming Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
+Normal rank
@@ Property / cites work @@
+Q4225152
@@ Property / cites work: Q4225152 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5713333
@@ Property / cites work: Q5713333 / rank @@
+Normal rank
@@ Property / cites work @@
+Howe's method for higher-order languages
@@ Property / cites work: Howe's method for higher-order languages / rank @@
+Normal rank
@@ Property / cites work @@
+Indexed codata types
@@ Property / cites work: Indexed codata types / rank @@
+Normal rank
@@ Property / cites work @@
+Proof search specifications of bisimulation and modal logics for the π-calculus
+Normal rank
@@ Property / cites work @@
+Cut elimination for a logic with induction and co-induction
+Normal rank