47 papers:
FoSSaCS-2015-CloustonBGB #induction #programming #reasoning #recursion- Programming and Reasoning with Guarded Recursion for Coinductive Types (RC, AB, HBG, LB), pp. 407–421.
RTA-2015-EndrullisHHP0 #equation #framework #induction #reasoning- A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (JE, HHH, DH, AP, AS), pp. 143–159.
ICALP-v2-2014-BonsangueRABR #algebra #induction- A Coalgebraic Foundation for Coinductive Union Types (MMB, JR, DA, FSdB, JJMMR), pp. 62–73.
ECOOP-2014-AnconaC #induction #object-oriented #type system- Sound and Complete Subtyping between Coinductive Types for Object-Oriented Languages (DA, AC), pp. 282–307.
POPL-2014-LagoSA #functional #higher-order #induction #on the #probability #source code- On coinductive equivalences for higher-order probabilistic functional programs (UDL, DS, MA), pp. 297–308.
ICLP-J-2014-MantadelisRM #exclamation #induction- Tabling, Rational Terms, and Coinduction Finally Together! (TM, RR, PM), pp. 429–443.
IJCAR-2014-Blanchette0T #induction #logic- Unified Classical Logic Completeness — A Coinductive Pearl (JCB, AP, DT), pp. 46–60.
LICS-CSL-2014-BonchiPPR #induction- Coinduction up-to in a fibrational setting (FB, DP, DP, JR), p. 9.
RTA-TLCA-2014-Czajka #confluence #induction #proving #λ-calculus- A Coinductive Confluence Proof for Infinitary λ-Calculus (LC), pp. 164–178.
LATA-2013-RotBR #equivalence #induction #proving- Coinductive Proof Techniques for Language Equivalence (JR, MMB, JJMMR), pp. 480–492.
PADL-2013-Moura #implementation #induction #logic programming #performance- A Portable and Efficient Implementation of Coinductive Logic Programming (PM), pp. 77–92.
POPL-2013-HurNDV #induction #power of #proving- The power of parameterization in coinductive proof (CKH, GN, DD, VV), pp. 193–206.
CSL-2013-Leivant #induction #semantics #type system- Global semantic typing for inductive and coinductive computing (DL), pp. 469–483.
FLOPS-2012-SaeedloeiG #constraints #induction #logic programming- Coinductive Constraint Logic Programming (NS, GG), pp. 243–259.
ECOOP-2012-Ancona #induction #object-oriented #semantics- Soundness of Object-Oriented Languages with Coinductive Big-Step Semantics (DA), pp. 459–483.
GCM-2010-PicardM11 #embedded #graph #induction #problem #representation- Coinductive Graph Representation: the Problem of Embedded Lists (CP, RM).
POPL-2011-HengleinN #axiom #induction #regular expression- Regular expression containment: coinductive axiomatization and computational interpretation (FH, LN), pp. 385–398.
ESOP-2010-NakataU #hoare #induction #logic #semantics- A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While (KN, TU), pp. 488–506.
FoSSaCS-2010-PopescuG #algebra #formal method #incremental #induction #process- Incremental Pattern-Based Coinduction for Process Algebra and Its Isabelle Formalization (AP, ELG), pp. 109–127.
LATA-2010-SaeedloeiG #induction #realtime #verification- Verifying Complex Continuous Real-Time Systems with Coinductive CLP(R) (NS, GG), pp. 536–548.
ECOOP-2009-AnconaL #induction #object-oriented #type system- Coinductive Type Systems for Object-Oriented Languages (DA, GL), pp. 2–26.
LOPSTR-2009-MinG #induction #logic programming- Coinductive Logic Programming with Negation (RM, GG), pp. 97–112.
LOPSTR-2009-Seki #induction #on the #proving- On Inductive and Coinductive Proofs via Unfold/Fold Transformations (HS), pp. 82–96.
CSL-2009-Berger #induction #proving- From Coinductive Proofs to Exact Real Arithmetic (UB), pp. 132–146.
RTA-2009-KimuraT #calculus #induction- Dual Calculus with Inductive and Coinductive Types (DK, MT), pp. 224–238.
ICALP-2007-SimonBMG #induction #logic programming- Co-Logic Programming: Extending Logic Programming with Coinduction (LS, AB, AM, GG), pp. 472–483.
ICLP-2007-GuptaBMSM #induction #logic programming- Coinductive Logic Programming and Its Applications (GG, AB, RM, LS, AM), pp. 27–44.
ESOP-2006-Leroy #induction #semantics- Coinductive Big-Step Operational Semantics (XL), pp. 54–68.
ICLP-2006-SimonMBG #induction #logic programming- Coinductive Logic Programming (LS, AM, AB, GG), pp. 330–345.
LICS-2006-Kozen #induction #probability #process #proving- Coinductive Proof Principles for Stochastic Processes (DK), pp. 359–366.
FASE-2005-HausmannMS #higher-order #induction- Iterative Circular Coinduction for CoCasl in Isabelle/HOL (DH, TM, LS), pp. 341–356.
PEPM-2002-BartheU #continuation #induction- CPS translating inductive and coinductive types (GB, TU), pp. 131–142.
FLOPS-2002-BarbosaO #calculus #induction #process- Coinductive Interpreters for Process Calculi (LSB, JNO), pp. 183–197.
CSL-2001-Matthes #induction #rank- Monotone Inductive and Coinductive Constructors of Rank 2 (RM), pp. 600–614.
LICS-2001-Jeffrey #induction #lts #type system- A Symbolic Labelled Transition System for Coinductive Subtyping of Fμ≤ Types (AJ), pp. 323–333.
ASE-2000-GoguenLR #induction- Circular Coinductive Rewriting (JAG, KL, GR), pp. 123–132.
WRLA-2000-GoguenLR #behaviour #induction- Behavioral and Coinductive Rewriting (JAG, KL, GR), pp. 2–23.
FoSSaCS-1999-Lenisa #bisimulation #equivalence #induction #logic- A Complete Coinductive Logical System for Bisimulation Equivalence on Circular Objects (ML), pp. 243–257.
ICALP-1999-Rutten #automaton #induction- Automata, Power Series, and Coinduction: Taking Input Derivatives Seriously (JJMMR), pp. 645–654.
WRLA-1998-MatsumotoF #automation #behaviour #induction #testing #towards #verification- Test set coinduction — Toward automated verification of behavioural properties (MM, KF), pp. 242–262.
CSL-1998-Altenkirch #induction #logic- Logical Relations and Inductive/Coinductive Types (TA), pp. 343–354.
LICS-1998-FernandezM #equivalence #induction #interactive- Coinductive Techniques for Operational Equivalence of Interaction Nets (MF, IM), pp. 321–332.
LICS-1998-PavlovicE #calculus #induction- Calculus in Coinductive Form (DP, MHE), pp. 408–417.
CADE-1997-DennisBG #bisimulation #induction #proving #using- Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs (LAD, AB, IG), pp. 276–290.
TLCA-1997-BrandtH #axiom #induction #recursion #similarity #type system- Coinductive Axiomatization of Recursive Type Equality and Subtyping (MB, FH), pp. 63–81.
TLCA-1997-Lenisa #induction #semantics #λ-calculus- Semantic Techniques for Deriving Coinductive Characterizations of Observational Equivalences for λ-calculi (ML), pp. 248–266.
ICFP-1996-Howard #induction- Inductive, Coinductive, and Pointed Types (BTH), pp. 102–109.