Automation for dependently typed functional programming

DOI10.3233/FI-2010-305MaRDI QIDQ3002482zbMATH OpenOpenAlexFDO

Authors Sean Wilson, Alan Smaill, Jacques D. Fleuriot

Publication date 20 May 2011

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-2010-305

zbMATH Keywords

dependent typesautomated theorem provingCoqripplinggeneralisation

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Dependently Typed Programming Based on Automated Theorem Proving
• How to make ad hoc proof automation less ad hoc
• How to make ad hoc proof automation less ad hoc
• An introduction to programming and proving with dependent types in Coq
• Auto in Agda. Programming proof search using reflection

Cited in

(3)

• Automated synthesis of functional programs with auxiliary functions
• Natural language inference in Coq
• Automatically proving equivalence by type-safe reflection

Describes a project that uses

Uses Software

• Cayenne
• QuickCheck
• Nuprl
• Coq

This page was built for publication: Automation for dependently typed functional programming

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