English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  Foundational Extensible Corecursion

Blanchette, J. C., Popescu, A., & Traytel, D. (2015). Foundational Extensible Corecursion. Retrieved from http://arxiv.org/abs/1501.05425.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0029-5B30-5 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0029-5B33-0
Genre: Paper

Files

show Files
hide Files
:
arXiv:1501.05425.pdf (Preprint), 316KB
View   Save
File Permalink:
https://hdl.handle.net/11858/00-001M-0000-0029-5B32-1
Name:
arXiv:1501.05425.pdf
Description:
File downloaded from arXiv at 2016-01-19 10:32
OA-Status:
Visibility:
Public
MIME-Type / Checksum:
application/pdf / [MD5]
Technical Metadata:
View
Copyright Date:
-
Copyright Info:
-
License:
http://arxiv.org/help/license

Locators

show

Creators

show
hide
 Creators:
Blanchette, Jasmin Christian1, Author           
Popescu, Andrei2, Author
Traytel, Dmitriy2, Author
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2External Organizations, ou_persistent22              

Content

show
hide
Free keywords: Computer Science, Programming Languages, cs.PL
 Abstract: This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under well-behaved operations, including constructors. Corecursive functions that are well behaved can be registered as such, thereby increasing the corecursor's expressiveness. The metatheory is formalized in the Isabelle proof assistant and forms the core of a prototype tool. The corecursor is derived from first principles, without requiring new axioms or extensions of the logic.

Details

show
hide
Language(s): eng - English
 Dates: 2015-01-222015-01-22
 Publication Status: Published online
 Pages: 12 p.
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: arXiv: 1501.05425
URI: http://arxiv.org/abs/1501.05425
BibTex Citekey: BlanchetteFoundArxiv15
 Degree: -

Event

show

Legal Case

show

Project information

show

Source

show