Document Open Access Logo

Observability for Pair Pattern Calculi

Authors Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca

Thumbnail PDF


  • Filesize: 0.51 MB
  • 15 pages

Document Identifiers

Author Details

Antonio Bucciarelli
Delia Kesner
Simona Ronchi Della Rocca

Cite AsGet BibTex

Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Observability for Pair Pattern Calculi. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 123-137, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)


Inspired by the notion of solvability in the λ-calculus, we define a notion of observability for a calculus with pattern matching. We give an intersection type system for such a calculus which is based on non-idempotent types. The typing system is shown to characterize the set of terms having canonical form, which properly contains the set of observable terms, so that typability alone is not sufficient to characterize observability. However, the inhabitation problem associated with our typing system turns out to be decidable, a result which — together with typability — allows to obtain a full characterization of observability.
  • solvability
  • pattern calculi
  • intersection types
  • inhabitation


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail