EasyChair Publications
PAR-10 Volume Information
Volume:Ekaterina Komendantskaya, Ana Bove and Milad Niqui (editors)
PAR-10. Partiality and Recursion in Interactive Theorem Provers

PAR-10 Volume Information

Title:PAR-10. Partiality and Recursion in Interactive Theorem Provers
Editors:Ekaterina Komendantskaya, Ana Bove and Milad Niqui
Series:EPiC Series in Computing
Publication date:May 15, 2012


Alexander KraussRecursive Definitions of Monadic Functions1-13
Conor McbrideDjinn, Monotonic14-17
Andreas AbelMiniAgda: Integrating Sized and Dependent Types18-33
Nils Anders DanielssonBeating the Productivity Checker Using Embedded Languages34-54
Issam Maamria and Michael ButlerRewriting and Well-Definedness within a Proof System55-71
Claudio Sacerdoti Coen and Silvio ValentiniGeneral Recursion and Formal Topology72-83
Aaron Stump, Vilhelm Sjöberg and Stephanie WeirichTermination Casts: A Flexible Approach to Termination with General Recursion84-100
Thorsten Altenkirch and Nils Anders DanielssonTermination Checking in the Presence of Nested Inductive and Coinductive Types101-106
Gavin Mendel-Gleason and Geoff HamiltonCyclic Proofs and Coinductive Principles107-113
Tarmo UustaluAntifounded Coinduction in Type Theory114


4dependent types
2coinduction, corecursion, general recursion, mixed induction and coinduction, type theory
1antifounded coinduction, corecursion, coinductive, constructive, event b, inductive, inductively generated formal topologies, partial functions, pattern matching, productivity, prover extensibility, recursion operator, sized types, subset, quotient types, term rewriting, termination, transition systems, types, well definedness, wellfounded induction, recursion