Browse
Publications
Preprints
About
About UCL Open: Env.
Aims and Scope
Editorial Board
Indexing
APCs
How to cite
Publishing policies
Editorial policy
Peer review policy
Equality, Diversity & Inclusion
About UCL Press
Contact us
For authors
Information for authors
How it works
Benefits of publishing with us
Submit
How to submit
Preparing your manuscript
Article types
Open Data
ORCID
APCs
Contributor agreement
For reviewers
Information for reviewers
Review process
How to peer review
Peer review policy
My ScienceOpen
Sign in
Register
Dashboard
Search
Browse
Publications
Preprints
About
About UCL Open: Env.
Aims and Scope
Editorial Board
Indexing
APCs
How to cite
Publishing policies
Editorial policy
Peer review policy
Equality, Diversity & Inclusion
About UCL Press
Contact us
For authors
Information for authors
How it works
Benefits of publishing with us
Submit
How to submit
Preparing your manuscript
Article types
Open Data
ORCID
APCs
Contributor agreement
For reviewers
Information for reviewers
Review process
How to peer review
Peer review policy
My ScienceOpen
Sign in
Register
Dashboard
Search
50
views
15
references
Top references
cited by
8
Cite as...
0 reviews
Review
0
comments
Comment
0
recommends
+1
Recommend
0
collections
Add to
0
shares
Share
Twitter
Sina Weibo
Facebook
Email
4,217
similar
All similar
Record
: found
Abstract
: not found
Book Chapter
: not found
Foundations of Software Science and Computation Structures
Guarded Dependent Type Theory with Coinductive Types
other
Author(s):
Aleš Bizjak
,
Hans Bugge Grathwohl
,
Ranald Clouston
,
Rasmus E. Møgelberg
,
Lars Birkedal
Publication date
(Print):
2016
Publisher:
Springer Berlin Heidelberg
Read this book at
Publisher
Further versions
open (via free pdf)
Powered by
Buy book
Review
Review book
Invite someone to review
Bookmark
Cite as...
There is no author summary for this book yet. Authors can add summaries to their books on ScienceOpen to make them more accessible to a non-specialist audience.
Related collections
Numerical Algebra, Matrix Theory, Differential-Algebraic Equations, and Control Theory
Most cited references
15
Record
: found
Abstract
: not found
Article
: not found
Idris, a general-purpose dependently typed programming language: Design and implementation
Edwin Brady
(2013)
0
comments
Cited
40
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Article
: not found
Applicative programming with effects
Conor McBride
,
ROSS PATERSON
(2008)
0
comments
Cited
25
times
– based on
0
reviews
Review now
Bookmark
Record
: found
Abstract
: not found
Conference Proceedings
: not found
Proving the correctness of reactive systems using sized types
John Hughes
,
Lars Pareto
,
Amr Sabry
(1996)
0
comments
Cited
20
times
– based on
0
reviews
Bookmark
All references
Author and book information
Book Chapter
Publication date (Print):
2016
Pages
: 20-35
DOI:
10.1007/978-3-662-49630-5_2
SO-VID:
44ae2081-d408-47b3-9547-fc2acd4670c2
License:
http://www.springer.com/tdm
History
Data availability:
Comments
Comment on this book
Sign in to comment
Book chapters
pp. 3
Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
pp. 20
Guarded Dependent Type Theory with Coinductive Types
pp. 55
Game Semantics for Bounded Polymorphism
pp. 73
Join Inverse Categories as Models of Reversible Recursion
pp. 91
A Coalgebraic View of Bar Recursion and Bar Induction
pp. 107
A New Foundation for Finitary Corecursion
pp. 126
Fixed-Point Elimination in the Intuitionistic Propositional Calculus
pp. 145
A Theory of Monitors
pp. 162
Contextual Approximation and Higher-Order Procedures
pp. 180
A Theory of Slicing for Probabilistic Control Flow Graphs
pp. 197
Verification of Parameterized Communicating Automata via Split-Width
pp. 217
Robust Equilibria in Mean-Payoff Games
pp. 234
Quantifier Alternation for Infinite Words
pp. 252
Synchronizing Automata over Nested Words
pp. 269
On Freeze LTL with Ordered Attributes
pp. 285
Regular Transformations of Data Words Through Origin Information
pp. 303
Trace Refinement in Labelled Markov Decision Processes
pp. 319
Qualitative Analysis of VASS-Induced MDPs
pp. 335
Metric Temporal Logic with Counting
pp. 353
Distributed Synthesis in Continuous Time
pp. 373
Unary Resolution: Characterizing Ptime
pp. 390
Focused and Synthetic Nested Sequents
pp. 408
Strong Normalizability as a Finiteness Structure via the Taylor Expansion of $$\lambda $$ λ -terms
pp. 424
Reasoning About Call-by-need by Means of Types
pp. 479
The Invariance Problem for Matrix Semigroups
pp. 493
Order-Sorted Rewriting and Congruence Closure
pp. 513
Towards a Formal Theory of Graded Monads
pp. 531
Profinite Monads, Profinite Equations, and Reiterman’s Theorem
Similar content
4,217
Coinduction in Control of Partially Observed Discrete-Event Systems
Authors:
Jan Komenda
A coalgebraic foundation for coinductive union types
Authors:
M. Bonsangue
,
J Rot
,
D ANCONA
…
Coinductive Definition of Distances between Processes: Beyond Bisimulation Distances
Authors:
David Romero-Hernández
,
David de Frutos-Escrig
See all similar
Cited by
8
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
Authors:
Alejandro Aguirre
,
Gilles Barthe
,
Lars Birkedal
…
Calculating Compilers for Concurrency
Authors:
Patrick Bahr
,
Graham Hutton
A Light Modality for Recursion
Authors:
Paula Severi
See all cited by