Context dependent procedures and computed types in \texttt{VeriFun}

DOI10.1016/J.ENTCS.2006.10.038MaRDI QIDQ2866336zbMATH OpenOpenAlexFDO

Authors Andreas Schlosser, Christoph Walther, Michael Gonder, Markus Aderhold

Publication date 13 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.10.038

zbMATH Keywords

computed typescontext dependencyreasoning on typessubtyping

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
• Verified functional programming of an abstract interpreter
• The geometry of types
• Automating relatively complete verification of higher-order functional programs
• scientific article; zbMATH DE number 2090721

Cites work

• Approximating the domains of functional and imperative programs
• Automated deduction -- CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 -- August 2, 2003. Proceedings
• scientific article; zbMATH DE number 43237 (Why is no real title available?)
• scientific article; zbMATH DE number 1552530 (Why is no real title available?)
• Reasoning About Incompletely Defined Programs
• Termination analysis for functional programs

Cited in

(3)

• Second-order programs with preconditions
• A two-valued logic for properties of strict functional programs allowing partial functions
• Reasoning about incompletely defined programs

Describes a project that uses

Uses Software

• VeriFun

This page was built for publication: Context dependent procedures and computed types in \texttt{VeriFun}

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