Dependent types and fibred computational effects

DOI10.1007/978-3-662-49630-5_3MaRDI QIDQ2811331zbMATH OpenOpenAlexFDO

Authors Danel Ahman, Neil Ghani, Gordon D. Plotkin

Publication date 10 June 2016

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

Full work available at URL http://link.springer.com/chapter/10.1007/978-3-662-49630-5_3

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Type theory (03B38)

Recommendations

• Dependent types in mathematical theory of programming
• Dependent inductive and coinductive types are fibrational dialgebras
• Normalization by evaluation and algebraic effects
• Fibrational modal type theory
• scientific article; zbMATH DE number 2090721

Cites work

• scientific article; zbMATH DE number 1670486 (Why is no real title available?)
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 2079022 (Why is no real title available?)
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)
• scientific article; zbMATH DE number 2087441 (Why is no real title available?)
• scientific article; zbMATH DE number 2120508 (Why is no real title available?)
• scientific article; zbMATH DE number 822489 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• A categorical semantics for linear logical frameworks
• A dependent type theory with abstractable names
• Algebras for parameterised monads
• Categorical logic and type theory
• Combining effects: sum and tensor
• Combining proofs and programs in a dependently typed language
• Continuous Lattices and Domains
• Countable Lawvere theories and computational effects
• Handling algebraic effects
• Hoare type theory, polymorphism and separation
• Indexed induction and coinduction, fibrationally
• Instances of computational effects: an algebraic perspective
• Integrating linear and dependent types
• Monadic parsing in Haskell
• Notions of computation and monads
• Programming and reasoning with algebraic effects and dependent types
• Semantics for algebraic operations
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• The enriched effect calculus: syntax and semantics

Cited in

(8)

• ν-Types for Effects and Freshness Analysis
• CHAD for expressive total languages
• A general semantic construction of dependent refinement type systems, categorically
• A classical sequent calculus with dependent types
• Gradual type theory
• Call-by-name gradual type theory
• An effectful way to eliminate addiction to dependence
• No value restriction is needed for algebraic effects and handlers

This page was built for publication: Dependent types and fibred computational effects

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