Type directed partial evaluation for level-1 shift and reset

MaRDI QIDQ4957791zbMATH OpenFDO

Authors Danko Ilik

Publication date 9 September 2021

Full work available at URL https://arxiv.org/abs/1210.2094, http://eptcs.web.cse.unsw.edu.au/paper.cgi?COS2013.6

Mathematics Subject Classification ID

Type theory (03B38) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1487847
• scientific article; zbMATH DE number 2090724
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• scientific article; zbMATH DE number 2018582
• scientific article; zbMATH DE number 177846

Cites work

• A compiled implementation of strong reduction
• Axioms for control operators in the CPS hierarchy
• Constructivism in mathematics. An introduction. Volume II
• Continuation-passing style models complete for intuitionistic logic
• Delimited control operators prove double-negation shift
• scientific article; zbMATH DE number 1555179 (Why is no real title available?)
• Kripke models for classical logic
• Representing Control: a Study of the CPS Transformation

Cited in

(1)

• scientific article; zbMATH DE number 2018582 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Type directed partial evaluation for level-1 shift and reset

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