From semantics to rules: a machine assisted analysis

DOI10.1007/BFB0049326MaRDI QIDQ4525278zbMATH OpenFDO

Authors Catarina Coquand

Publication date 22 January 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0049326

Mathematics Subject Classification ID

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

Cited in

(9)

• Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
• On explicit substitutions and names (extended abstract)
• Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
• Type directed partial evaluation for level-1 shift and reset
• Categorical reconstruction of a reduction free normalization proof
• POPLMark reloaded: mechanizing proofs by logical relations
• Semantic analysis of normalisation by evaluation for typed lambda calculus
• Kripke models for classical logic
• Program extraction from normalization proofs

Describes a project that uses

Uses Software

• ALF

This page was built for publication: From semantics to rules: a machine assisted analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4525278)