Partiality, state and dependent types

DOI10.1007/978-3-642-21691-6_17MaRDI QIDQ3007667zbMATH OpenOpenAlexFDO

Authors Kasper Svendsen, Aleksandar Nanevski, Lars Birkedal

Publication date 17 June 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-21691-6_17

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 1303347
• Partiality and recursion in interactive theorem provers -- an overview
• HYBRID PARTIAL-TOTAL TYPE THEORY
• Partiality, Revisited
• Remarks on Martin-Löf's partial type theory

Cites work

• A Realizability Model for Impredicative Hoare Type Theory
• An introduction to small scale reflection in Coq
• Automata, Languages and Programming
• Categorical logic and type theory
• General Recursion via Coinductive Types
• Hoare type theory, polymorphism and separation
• scientific article; zbMATH DE number 1303347 (Why is no real title available?)
• scientific article; zbMATH DE number 1105469 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• Interacting with Modal Logics in the Coq Proof Assistant
• Partiality, state and dependent types
• Proof of correctness of data representations
• Realisability semantics of parametric polymorphism, general references and recursive types
• Recursion over realizability structures
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Simple general recursion in type theory
• Structuring the verification of heap-manipulating programs
• The Vienna development method: The meta-language
• Wellfounded trees in categories
• Ynot: dependent types for imperative programs

Cited in

(4)

• Type theory and language constructs for objects with states
• Partiality, state and dependent types
• scientific article; zbMATH DE number 1303347 (Why is no real title available?)
• Dependent types ensure partial correctness of theorem provers

Describes a project that uses

Uses Software

• Coq
• Eiffel
• Ynot

This page was built for publication: Partiality, state and dependent types

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