Reynolds, AndrewBlanchette, Jasmin Christian2015-12-022015-12-022015-12-02201510.1007/978-3-319-21401-6_13https://infoscience.epfl.ch/handle/20.500.14299/121337WOS:000363947500013We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson-Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from theories developed with Isabelle demonstrates the potential of the procedure.text::conference output::conference proceedings::conference paper