scientific article; zbMATH DE number 7761007

DOI10.4230/lipics.types.2017.4zbMath1528.68083arXiv1901.03208MaRDI QIDQ6060675

Rodolphe Lepigre

Publication date: 3 November 2023

Full work available at URL: https://arxiv.org/abs/1901.03208

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

classical logicprogram verificationCurry-style quantificationimplicit subtypingML-like languagetermination checking

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The calculus of constructions
• A syntactic approach to type soundness
• Getting results from programs extracted from classical proofs
• A Classical Realizability Model for a Semantical Value Restriction
• Dependently Typed Programming in Agda
• Program verification through characteristic formulae
• Characteristic formulae for the verification of imperative programs
• AURA
• The size-change principle for program termination
• Call-by-value is dual to call-by-name
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions
• Secure distributed programming with value-dependent types
• Combining proofs and programs in a dependently typed language
• Types for Proofs and Programs
• Semi-continuous Sized Types and Termination
• Analysis 2

This page was built for publication: