scientific article; zbMATH DE number 7437716

zbMath1476.68056arXiv1509.03021MaRDI QIDQ5014449

Tom Schrijvers, Paolo Torrini

Publication date: 2 December 2021

Full work available at URL: https://arxiv.org/abs/1509.03021

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Uses Software

• Coq
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The calculus of constructions
• Iteration and coiteration schemes for higher-order and nested datatypes
• The origins of structural operational semantics
• Inductive types and type constraints in the second-order lambda calculus
• Meta-theory à la carte
• Data types à la carte
• A tutorial on the universality and expressiveness of fold
• Ott: Effective tool support for the working semanticist
• Modular monadic meta-theory
• Programming Languages and Systems
• Inductively defined types in the Calculus of Constructions