Refinement types for program analysis

DOI10.1007/3-540-61739-6_39MaRDI QIDQ5030192zbMATH OpenOpenAlexFDO

Authors Mario Coppo, Ferruccio Damiani, Paola Giannini

Publication date 16 February 2022

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61739-6_39

zbMATH Keywords

binding timefaithful refinementfaithful typingtype assignmenttype inference

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1301731
• Program and proof optimizations with type systems
• Automatic useless-code elimination for HOT functional programs
• A conjunctive type system for useless-code elimination
• scientific article; zbMATH DE number 1361535

Cites work

• A filter lambda model and the completeness of type assignment
• A theory of type polymorphism in programming
• An extension of basic functionality theory for -calculus
• scientific article; zbMATH DE number 2185653 (Why is no real title available?)
• scientific article; zbMATH DE number 1479641 (Why is no real title available?)
• Principal types and unification for simple intersection type systems
• Pruning simply typed  -terms
• Strictness and totality analysis
• The Principal Type-Scheme of an Object in Combinatory Logic
• Type inference, abstract interpretation and strictness analysis

Cited in

(18)

• LP structures on type lattices and some refactoring problems
• Eliminating dead code on recursive data.
• Automatic useless-code elimination for HOT functional programs
• Refinement types for Haskell
• Learning refinement types
• A conjunctive type system for useless-code elimination
• scientific article; zbMATH DE number 1953279 (Why is no real title available?)
• scientific article; zbMATH DE number 2080290 (Why is no real title available?)
• scientific article; zbMATH DE number 1738289 (Why is no real title available?)
• scientific article; zbMATH DE number 1361535 (Why is no real title available?)
• An effective theory of type refinements
• On-Demand Refinement of Dependent Types
• Type Reconstruction for General Refinement Types
• ICE-based refinement type discovery for higher-order functional programs
• ICE-based refinement type discovery for higher-order functional programs
• On average-case hardness of higher-order model checking
• Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
• Program and proof optimizations with type systems

This page was built for publication: Refinement types for program analysis

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