2023/04/17 by Gilles Dowek, Dowek, Gilles
Computer Science · #Advanced Algebra and Logic #Constraint Satisfaction and Optimization #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2304.08068
openalex publication_date 2023/04/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Instead of developing a customized typed lambda-calculus for each theory, we attempt to design a general parametric calculus that permits to express the proofs of any theory. This way, the problem of expressing proofs in the lambda-calculus is separated from that of choosing a theory.