Dependent types from counterexamples

DOI10.1145/1706299.1706315MaRDI QIDQ5255067zbMATH OpenOpenAlexFDO

Authors Tachio Terauchi

Publication date 11 June 2015

Published in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.180.9289

zbMATH Keywords

counterexamplesdependent typesinterpolationintersection typestype inference

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On-Demand Refinement of Dependent Types
• Dependent array type inference from tests
• Dependent Types for Low-Level Programming
• Compositional and lightweight dependent type inference for ML
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(13)

• Sound and complete concolic testing for higher-order functions
• Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking
• Compositional and lightweight dependent type inference for ML
• Modular verification of higher-order functional programs
• Dependent array type inference from tests
• Higher order symbolic execution for contract verification and refutation
• On-Demand Refinement of Dependent Types
• Tools and Algorithms for the Construction and Analysis of Systems
• State of the Union: Type Inference Via Craig Interpolation
• ICE-based refinement type discovery for higher-order functional programs
• Manifest contracts with intersection types
• On recursion-free Horn clauses and Craig interpolation
• Constraint-based relational verification

Describes a project that uses

Uses Software

• SLAM
• OCaml

This page was built for publication: Dependent types from counterexamples

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