Supercompilation for Martin-Lof's type theory

DOI10.1134/S0361768815030068zbMATH Open1339.68042MaRDI QIDQ300348FDOQ300348

Authors: I. G. Klyuchnikov, S. A. Romanenko 

Publication date: 27 June 2016

Published in: Programming and Computer Software (Search for Journal in Brave)

Recommendations

• Certifying supercompilation for Martin-Löf's type theory
• The concept of a supercompiler
• scientific article; zbMATH DE number 3943000
• A positive supercompiler
• scientific article; zbMATH DE number 1630107

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cites Work

• The concept of a supercompiler
• Title not available (Why is that?)
• Higher-level supercompilation as a metasystem transition
• Verification as a parameterized testing (experiments with the SCP4 supercompiler)
• Practical foundations for programming languages
• A tutorial implementation of a dependently typed lambda calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• A tutorial on the universality and expressiveness of fold

Cited In (10)

• Positive supercompilation for a higher order call-by-value language
• Intermediate representation of programs with type specification based on pattern matching
• The strength of Martin-Löf type theory with a superuniverse. I
• Polynomial-time Martin-Löf type theory
• Positive supercompilation for a higher-order call-by-value language
• The concept of a supercompiler
• Title not available (Why is that?)
• Supercompilation for datatypes
• Title not available (Why is that?)
• Certifying supercompilation for Martin-Löf's type theory

Uses Software

• Coq
• Refal

This page was built for publication: Supercompilation for Martin-Lof's type theory

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