Ideograph: A Language for Expressing and Manipulating Structured Data

We introduce Ideograph, a language for expressing and manipulating structured data. Its types describe kinds of structures, such as natural numbers, lists, multisets, binary trees, syntax trees with variable binding, directed multigraphs, and relational databases. Fully normalized terms of a type correspond exactly to members of the structure, analogous to a Church-encoding. Moreover, definable operations over these structures are guaranteed to respect the structures' equivalences. In this paper, we give the syntax and semantics of the non-polymorphic subset of Ideograph, and we demonstrate how it can represent and manipulate several interesting structures.

• Publication year

  2023

• Venue

  TERMGRAPH@FSCD

• Publication date

  2023-03-25

• Fields of study

  Computer Science

• Identifiers
  DOI 10.4204/EPTCS.377.4arXiv 2303.15784
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Revisiting Graph Types in HyperLMNtal: A Modeling Language for Hypergraph Rewriting

  2021cited by this paper
• Logic Beyond Formulas: A Proof System on Graphs

  2020cited by this paper
• Modeling Terms by Graphs with Structure Constraints (Two Illustrations)

  2019cited by this paper
• The Bang Calculus and the Two Girard's Translations

  2019cited by this paper
• Labelled Port Graph - A Formal Structure for Models and Computations

  2018cited by this paper
• The Design of GP 2

  2012cited by this paper
• Functional programming with structured graphs

  2012cited by this paper
• Proceedings 10th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2011, Novi Sad, Serbia, 29 May 2011

  2011cited by this paper
• LMNtal as a hierarchical logic programming language

  2009cited by this paper
• An Interaction Net Implementation of Closed Reduction

  2008cited by this paper
• Parametric higher-order abstract syntax for mechanized semantics

  2008cited by this paper
• Mechanized Metatheory for the Masses: The PoplMark Challenge

  2005cited by this paper
• The GROOVE Simulator: A Tool for State Space Generation

  2003cited by this paper
• Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism

  2003cited by this paper
• Handsome proof-nets: perfect matchings and cographs

  2003cited by this paper
• Interaction nets for linear logic

  2000cited by this paper
• A Categorical and Graphical Treatment of Closure Conversion

  1999cited by this paper
• From proof-nets to interaction nets

  1995cited by this paper
• Second Order Isomorphic Types: A Proof Theoretic Study on Second Order λ-Calculus with Surjective Pairing and Terminal Object

  1995cited by this paper
• The geometry of implementation

  1994cited by this paper
• Computational Interpretations of Linear Logic

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

  1992cited by this paper
• Linear logic

  1992cited by this paper
• A formulae-as-type notion of control

  1989cited by this paper
• Interaction nets

  1989cited by this paper
• Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem

  1972cited by this paper

• Opportunistically Parallel Lambda Calculus

  2024cites this paper