Dependent types and fibred computational effects

DOI10.1007/978-3-662-49630-5_3zbMATH Open1475.68057OpenAlexW2460339236MaRDI QIDQ2811331FDOQ2811331

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

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

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)

Cites Work

• Categorical logic and type theory
• Combining effects: sum and tensor
• Title not available (Why is that?)
• Title not available (Why is that?)
• Continuous Lattices and Domains
• Title not available (Why is that?)
• Instances of Computational Effects: An Algebraic Perspective
• Title not available (Why is that?)
• Notions of computation and monads
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Hoare type theory, polymorphism and separation
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
• Title not available (Why is that?)
• Title not available (Why is that?)
• A dependent type theory with abstractable names
• Semantics for Algebraic Operations
• Handling algebraic effects
• Programming and reasoning with algebraic effects and dependent types
• Countable Lawvere theories and computational effects
• Algebras for Parameterised Monads
• A Categorical Semantics for Linear Logical Frameworks
• Integrating linear and dependent types
• Combining proofs and programs in a dependently typed language
• Monadic parsing in Haskell
• Indexed induction and coinduction, fibrationally
• The enriched effect calculus: syntax and semantics

Cited In (7)

• ν-Types for Effects and Freshness Analysis
• CHAD for expressive total languages
• A general semantic construction of dependent refinement type systems, categorically
• Gradual type theory
• Title not available (Why is that?)
• A Classical Sequent Calculus with Dependent Types
• 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)