Supercompilation for Martin-Lof's type theory

DOI10.1134/S0361768815030068zbMath1339.68042MaRDI QIDQ300348

I. G. Klyuchnikov, S. A. Romanenko

Publication date: 27 June 2016

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

Mathematics Subject Classification ID

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

Related Items

Intermediate representation of programs with type specification based on pattern matching

Uses Software

• Coq
• Refal

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• The concept of a supercompiler
• A tutorial on the universality and expressiveness of fold