Elegant elaboration with function invocation
Programming Languages
2021-07-07 v3
Authors:
Tesla Zhang
Abstract
We present an elegant design of the core language in a dependently-typed lambda calculus with δ-reduction and an elaboration algorithm.
Cite
@article{arxiv.2105.14840,
title = {Elegant elaboration with function invocation},
author = {Tesla Zhang},
journal= {arXiv preprint arXiv:2105.14840},
year = {2021}
}
Comments
6 pages, 3 figures
Related papers
View all related →
Programming Languages · Computer Science
Reduction Strategies in the Lambda Calculus and Their Implementation through Derivable Abstract Machines: Introduction
Tomasz Drab
2024-05-22
Programming Languages · Computer Science
Abductive functional programming, a semantic approach
Koko Muroya, Steven Cheung, Dan R. Ghica
2017-10-12
Logic in Computer Science · Computer Science
A lambda calculus for quantum computation with classical control
Peter Selinger, Benoit Valiron
2009-02-26
Logic in Computer Science · Computer Science
A strong call-by-need calculus
Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond
2023-06-22
Logic in Computer Science · Computer Science
Elaboration in Dependent Type Theory
Leonardo de Moura, Jeremy Avigad, Soonho Kong, Cody Roux
2015-12-18
Logic in Computer Science · Computer Science
A call-by-value lambda-calculus with lists and control
Robbert Krebbers
2012-10-12
Programming Languages · Computer Science
Semantics of a Relational {\lambda}-Calculus (Extended Version)
Pablo Barenbaum, Federico Lochbaum, Mariana Milicich
2021-03-02
Logic in Computer Science · Computer Science
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, Lars Birkedal
2019-03-14
Programming Languages · Computer Science
$\mu\lambda\epsilon\delta$-Calculus: A Self Optimizing Language that Seems to Exhibit Paradoxical Transfinite Cognitive Capabilities
Ronie Salgado
2024-09-10
Logic in Computer Science · Computer Science
A Probabilistic Call-by-Need Lambda-Calculus -- Extended Version
David Sabel, Manfred Schmidt-Schauß, Luca Maio
2022-05-31
Programming Languages · Computer Science
Programming and Reasoning with Guarded Recursion for Coinductive Types
Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, Lars Birkedal
2015-01-16
Logic in Computer Science · Computer Science
A Tutorial Introduction to the Lambda Calculus
Raul Rojas
2015-04-01
Programming Languages · Computer Science
Call-By-Name Is Just Call-By-Value with Delimited Control
Mateusz Pyzik
2023-06-22
Logic in Computer Science · Computer Science
The Formal System lambda-delta
F. Guidi
2008-09-25
Programming Languages · Computer Science
The Functional Machine Calculus III: Control
Willem Heijltjes
2026-03-03
Programming Languages · Computer Science
A Lambda-Calculus with letrec, case, constructors and non-determinism
Manfred Schmidt-Schauß, Michael Huber
2007-05-23
Logic in Computer Science · Computer Science
A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi
Andrew Gacek, Gopalan Nadathur
2007-05-23
Logic in Computer Science · Computer Science
Infinitary $\lambda$-Calculi from a Linear Perspective (Long Version)
Ugo Dal Lago
2016-04-29
Programming Languages · Computer Science
A Theory of Changes for Higher-Order Languages - Incrementalizing {\lambda}-Calculi by Static Differentiation
Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, Klaus Ostermann
2013-12-04
Programming Languages · Computer Science
Compiling Purely Functional Structured Programs
Phil Scott, Steven Obua, Jacques Fleuriot
2017-03-17
Logic in Computer Science · Computer Science
Quantum Lambda Calculi with Classical Control: Syntax and Expressive Power
Ugo Dal Lago, Andrea Masini, Margherita Zorzi
2007-05-23
Programming Languages · Computer Science
A Theory of Explicit Substitutions with Safe and Full Composition
Delia Kesner
2015-07-01
Logic in Computer Science · Computer Science
On the Invariance of the Unitary Cost Model for Head Reduction (Long Version)
Beniamino Accattoli, Ugo Dal Lago
2012-02-09
Logic in Computer Science · Computer Science
Extending the Applicability Condition in the Formal System $\lambda\delta$
Ferruccio Guidi
2019-12-02
Programming Languages · Computer Science
A Proposal for an Interactive Shell Based on a Typed Lambda Calculus
Kouji Matsui
2021-04-09