To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Well-founded recursion ov… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Well-founded recursion over contextual objects

Conference paper
Authors Brigitte Pientka
Andreas Abel
Published in Leibniz International Proceedings in Informatics, LIPIcs
ISSN 1868-8969
Publication year 2015
Published at Department of Computer Science and Engineering (GU)
Language en
Keywords Dependent types, Logical frameworks, Type systems
Subject categories Computer and Information Science


© Brigitte Pientka and Andreas Abel;.We present a core programming language that supports writing well-founded structurally recursive functions using simultaneous pattern matching on contextual LF objects and contexts. The main technical tool is a coverage checking algorithm that also generates valid recursive calls. To establish consistency, we define a call-by-value small-step semantics and prove that every well-typed program terminates using a reducibility semantics. Based on the presented methodology we have implemented a totality checker as part of the programming and proof environment Beluga where it can be used to establish that a total Beluga program corresponds to a proof.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?