Copatterns: programming infinite structures by observations

No abstract is available for this paper.

• Publication year

  2013

• Venue

  ACM-SIGACT Symposium on Principles of Programming Languages

• Publication date

  2013-01-23

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/2429069.2429075
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Coalgebras as Types Determined by Their Elimination Rules

  2012cited by this paper
• Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types

  2012influential reference
• Subtyping, declaratively: an exercise in mixed induction and coinduction

  2010cited by this paper
• Termination Checking in the Presence of Nested Inductive and Coinductive Types

  2010influential reference
• Subtyping, Declaratively

  2010cited by this paper
• Dual Calculus with Inductive and Coinductive Types

  2009influential reference
• Focusing on pattern matching

  2009cited by this paper
• The logical basis of evaluation order and pattern-matching

  2009cited by this paper
• Let's See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)

  2009cited by this paper
• On the unity of duality

  2008cited by this paper
• Case Analysis of Higher-Order Data

  2008influential reference
• Focusing on Binding and Computation

  2008cited by this paper
• Focusing and higher-order abstract syntax

  2008cited by this paper
• Reference and Computation in Intuitionistic Type Theory

  2008cited by this paper
• Mixed Inductive/Coinductive Types and Strong Normalization

  2007cited by this paper
• Eliminating Dependent Pattern Matching

  2006cited by this paper
• Call-by-Value Is Dual to Call-by-Name - Reloaded

  2005influential reference
• Semantic types: a fresh look at the ideal model for types

  2004cited by this paper
• Call-by-value is dual to call-by-name

  2003cited by this paper
• A Coverage Checking Algorithm for LF

  2003cited by this paper
• The duality of computation

  2000influential reference
• The coq proof assistant reference manual

  2000cited by this paper
• Local type inference

  1998cited by this paper
• Proofs of strong normalisation for second order classical natural deduction

  1997cited by this paper
• Proving the correctness of reactive systems using sized types

  1996influential reference
• Un calcul de constructions infinies et son application a la verification de systemes communicants

  1996cited by this paper
• A Syntactic Approach to Type Soundness

  1994cited by this paper
• A Theory of Primitive Objects - Untyped and First-Order Systems

  1994cited by this paper
• A Term Calculus for Intuitionistic Linear Logic

  1993cited by this paper
• Logic Programming with Focusing Proofs in Linear Logic

  1992cited by this paper
• Pattern Matching with Dependent Types

  1992cited by this paper
• Codatatypes in ML

  1989influential reference
• A Typed Lambda Calculus with Categorical Type Constructors

  1987cited by this paper
• Infinite Objects in Type Theory

  1986cited by this paper
• A view from the left

  1984cited by this paper
• A Theory of Type Polymorphism in Programming

  1978cited by this paper
• Íòòòö Óò××××öøøóò Óö Ôùùðð Blockinøøóò Ò Ååøøº Ëøöù Blockinøº Ò Óñôº Ë Blockin Blockin Blockinò Ìýô¹¹¹××× Øøöññòòøøóò Óó Öö Blockinùö××ú ¬òòøøóò×

  year unknowncited by this paper

• Hyperfunctions: Communicating Continuations

  2026cites this paper
• Filling the Gaps of Polarity: Implementing Dependent Data and Codata Types with Implicit Arguments

  2025cites this paper
• Controlling Copatterns: There and Back Again

  2025cites this paper
• The Conatural Numbers Form an Exponential Commutative Semiring

  2025cites this paper
• Notions of Stack-Manipulating Computation and Relative Monads

  2025cites this paper
• Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation

  2025cites this paper
• A contextual formalization of structural coinduction

  2025cites this paper
• Formalising Graph Algorithms with Coinduction

  2025cites this paper
• Programming with Dependent Additive Pairs

  2024cites this paper
• Grokking the Sequent Calculus (Functional Pearl)

  2024cites this paper
• Amortized Analysis via Coalgebra

  2024cites this paper
• Deriving Dependently-Typed OOP from First Principles

  2024cites this paper
• Modal μ-Calculus for Free in Agda

  2024cites this paper
• Call-by-Unboxed-Value

  2024cites this paper
• Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

  2024cites this paper
• Amortized Analysis via Coinduction

  2023cites this paper
• Dependent Type Refinements for Futures

  2023cites this paper
• Some techniques for reasoning automatically on co-inductive data structures

  2023cites this paper
• Live Pattern Matching with Typed Holes

  2023cites this paper
• A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈

  2023cites this paper
• Inductive Reasoning for Coinductive Types

  2023cites this paper
• Scoped and Typed Staging by Evaluation

  2023cites this paper
• Structural refinement types

  2022cites this paper
• A Bowtie for a Beast (Technical Appendix)

  2022influential citation
• Data-Codata Symmetry and its Interaction with Evaluation Order

  2022cites this paper
• Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs

  2022cites this paper
• Introduction and elimination, left and right

  2022cites this paper
• Symbolic and automatic differentiation of languages

  2021cites this paper
• A Mechanized Semantic Metalanguage for High Level Synthesis

  2021cites this paper
• Inductive and Coinductive Predicate Liftings for Effectful Programs

  2021cites this paper
• Flexible Coinduction in Agda

  2021cites this paper
• The Multiverse: Logical Modularity for Proof Assistants

  2021cites this paper
• Higher Lenses

  2021cites this paper
• Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor

  2021cites this paper
• Classical (co)recursion: Mechanics

  2021cites this paper
• Classical (Co)Recursion: Programming

  2021influential citation
• Synthetic Spectra via a Monadic and Comonadic Modality

  2021cites this paper
• On the Proof Theory of Property-Based Testing of Coinductive Specifications, or: PBT to Infinity and beyond

  2020cites this paper
• Efficient lambda encodings for Mendler-style coinductive types in Cedille

  2020cites this paper
• Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part II

  2020cites this paper
• Flexible Coinduction in Agda

  2020cites this paper
• A Computational Understanding of Classical (Co)Recursion

  2020cites this paper
• Programming Metamorphic Algorithms: An Experiment in Type-Driven Algorithm Design

  2020cites this paper
• Intuitionistic Fixed Point Logic

  2020cites this paper
• Elaborating inductive definitions in Curry-style polymorphic type theory

  2020cites this paper
• Well-definedness and observational equivalence for inductive-coinductive programs

  2019influential citation
• Cubical agda: a dependently typed programming language with univalence and higher inductive types

  2019cites this paper
• Exploring Codata : The Relation to Object-Orientation

  2019cites this paper
• Totality for Mixed Inductive and Coinductive Types

  2019cites this paper
• The Size-Change Principle for Mixed Inductive and Coinductive types

  2019cites this paper
• Coq Coq correct! verification of type checking and erasure for Coq, in Coq

  2019cites this paper
• Squeezing Streams and Composition of Self-stabilizing Algorithms

  2019cites this paper
• Guarded Recursion in Agda via Sized Types

  2019cites this paper
• Transformations for Generating Type Refinements

  2019cites this paper
• Decomposition diversity with symmetric data and codata

  2019influential citation
• Coinduction in Flow: The Later Modality in Fibrations

  2019cites this paper
• Engineering formal systems in constructive type theory

  2019cites this paper
• POPLMark reloaded: Mechanizing proofs by logical relations

  2019cites this paper
• Codata in Action

  2019influential citation
• Dependent Pearl: Normalization by realizability

  2019cites this paper
• Dualizing Generalized Algebraic Data Types by Matrix Transposition

  2018influential citation
• Almost Sure Productivity

  2018cites this paper
• A case study in programming coinductive proofs: Howe’s method

  2018influential citation
• Elaborating dependent (co)pattern matching

  2018cites this paper
• Sailing Routes in the World of Computation

  2018cites this paper
• A type and scope safe universe of syntaxes with binding: their semantics and proofs

  2018cites this paper
• Keep your laziness in check

  2018cites this paper
• Optimized Program Extraction for Induction and Coinduction

  2018cites this paper
• Coaxioms: flexible coinductive definitions by inference systems

  2018cites this paper
• Declarative GUIs: Simple, Consistent, and Verified

  2018cites this paper
• Developing GUI Applications in a Verified Setting

  2018cites this paper
• Undecidability of Equality for Codata Types

  2018cites this paper
• 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, May 23-26, 2016

  2018cites this paper
• Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

  2018cites this paper
• Keep Your Laziness in Check 102 : 3 1 . 2 Describing Strictness , and Testing It !

  2018cites this paper
• Copattern matching and first-class observations in OCaml, with a macro

  2017cites this paper
• Type-and-scope safe programs and their proofs

  2017cites this paper
• Relational Graph Models at Work

  2017cites this paper
• Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis

  2017cites this paper
• Up-to techniques using sized types

  2017cites this paper
• Metadata of the chapter that will be visualized in SpringerLink

  2017cites this paper
• Observational Equivalence for Behavioural Differential Equations

  2017cites this paper
• Trace and Stable Failures Semantics for CSP-Agda

  2017cites this paper
• CoCaml: Functional Programming with Regular Coinductive Types

  2017cites this paper
• Interactive programming in Agda – Objects and graphical user interfaces

  2017cites this paper
• The continuity of monadic stream functions

  2017cites this paper
• The clocks are ticking: No more delays!

  2017cites this paper
• Generalizing Inference Systems by Coaxioms

  2017cites this paper
• agdarsec -- Total Parser Combinators

  2017cites this paper
• Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants

  2016cites this paper
• Type Theory based on Dependent Inductive and Coinductive Types

  2016cites this paper
• Indexed codata types

  2016cites this paper
• Formal Languages, Formally and Coinductively

  2016cites this paper
• Contractive Functions on Infinite Data Structures

  2016cites this paper
• Dualized Simple Type Theory

  2016cites this paper
• How to Reason Coinductively Informally

  2016influential citation
• Defining Trace Semantics for CSP-Agda

  2016cites this paper
• Infinitary Proof Theory: the Multiplicative Additive Case

  2016cites this paper
• A realizability interpretation of Church's simple theory of types

  2016cites this paper
• Programming with monadic CSP-style processes in dependent type theory

  2016cites this paper