Interactive programming in Agda -- objects and graphical user interfaces

DOI10.1017/S0956796816000319zbMATH Open1418.68031OpenAlexW2552040597MaRDI QIDQ5372002FDOQ5372002

Andreas Abel, Anton Setzer, Stephan Adelsberger

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796816000319

Recommendations

• scientific article; zbMATH DE number 1670486
• scientific article; zbMATH DE number 2247254
• State dependent IO-monads in type theory
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Types for Proofs and Programs

Mathematics Subject Classification ID

Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35) Functional programming and lambda calculus (68N18)

Cites Work

• Programming with algebraic effects and handlers
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Notions of computation and monads
• Title not available (Why is that?)
• Inductive families
• A predicative analysis of structural recursion
• Typestate: A programming language concept for enhancing software reliability
• Title not available (Why is that?)
• Title not available (Why is that?)
• The view from the left
• Type-based termination of recursive definitions
• Safe functional reactive programming through dependent types
• Codatatypes in ML
• Title not available (Why is that?)
• Inductive-Inductive Definitions
• A set constructor for inductive sets in Martin-Löf's type theory
• Rewriting Techniques and Applications
• Typed Lambda Calculi and Applications
• Title not available (Why is that?)
• Induction-recursion and initial algebras.
• Foundational extensible corecursion: a proof assistant perspective
• Copatterns
• How to Reason Coinductively Informally
• Coalgebras as Types Determined by Their Elimination Rules
• Tarski's fixed-point theorem and lambda calculi with monotone inductive types
• Indexed containers
• Semi-continuous Sized Types and Termination
• Small Induction Recursion
• Title not available (Why is that?)
• Type-Based Termination with Sized Products
• Programming interfaces and basic topology
• Wellfounded recursion with copatterns
• Title not available (Why is that?)
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• Mixed Inductive/Coinductive Types and Strong Normalization
• Title not available (Why is that?)

Cited In (4)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Programming graphical user interfaces with Scheme
• Undecidability of equality for codata types

Uses Software

• Coq
• Haskell
• Agda
• wxHaskell
• MiniAgda
• Eff
• GitHub

This page was built for publication: Interactive programming in Agda -- objects and graphical user interfaces

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