Internal models of system F for decompilation

DOI10.1016/J.TCS.2012.02.022zbMath1244.68025OpenAlexW2008950540MaRDI QIDQ428882

Stefano Berardi, Makoto Tatsuta

Publication date: 25 June 2012

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2012.02.022

zbMATH Keywords

compilerde Bruijn leveldecompilersemantics of polymorphismsystem Ftyped \(\lambda \)-calculus

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Cites Work

• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The system \({\mathcal F}\) of variable types, fifteen years later
• Building continuous webbed models for system F
• A full continuous model of polymorphism
• Simple Types in Type Theory: Deep and Shallow Encodings
• Typed Applicative Structures and Normalization by Evaluation for System F ω
• Constructive natural deduction and its ‘ω-set’ interpretation
• βη-complete models for System F
• Operational aspects of untyped Normalisation by Evaluation
• Explicit substitutions with de bruijn's levels
• Weak βη-Normalization and Normalization by Evaluation for System F

This page was built for publication: Internal models of system F for decompilation