Relevant bibliographies by topics / Lambda-Pi calculus

Contents

  1. Journal articles
  2. Dissertations / Theses
  3. Book chapters
  4. Conference papers

Academic literature on the topic 'Lambda-Pi calculus'

Author: Grafiati
Published: 25 May 2024
Last updated: 31 July 2025

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles

Select a source type:

Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'Lambda-Pi calculus.'

Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.

You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.

Journal articles on the topic "Lambda-Pi calculus"

1

van Bakel, Steffen, and Maria Grazia Vigliotti. "A fully-abstract semantics of lambda-mu in the pi-calculus." Electronic Proceedings in Theoretical Computer Science 164 (September 9, 2014): 33–47. http://dx.doi.org/10.4204/eptcs.164.3.

Full text
APA, Harvard, Vancouver, ISO, and other styles
2

Fu, Weili, Fabian Krause, and Peter Thiemann. "Label dependent lambda calculus and gradual typing." Proceedings of the ACM on Programming Languages 5, OOPSLA (2021): 1–29. http://dx.doi.org/10.1145/3485485.

Full text
Abstract:
Dependently-typed programming languages are gaining importance, because they can guarantee a wide range of properties at compile time. Their use in practice is often hampered because programmers have to provide very precise types. Gradual typing is a means to vary the level of typing precision between program fragments and to transition smoothly towards more precisely typed programs. The combination of gradual typing and dependent types seems promising to promote the widespread use of dependent types. We investigate a gradual version of a minimalist value-dependent lambda calculus. Compile-tim
APA, Harvard, Vancouver, ISO, and other styles
3

Laustsen, Niels Jakob, and Vladimir G. Troitsky. "Vector Lattices Admitting a Positively Homogeneous Continuous Function Calculus." Quarterly Journal of Mathematics 71, no. 1 (2020): 281–94. http://dx.doi.org/10.1093/qmathj/haz031.

Full text
Abstract:
Abstract We characterize the Archimedean vector lattices that admit a positively homogeneous continuous function calculus by showing that the following two conditions are equivalent for each $n$-tuple $\boldsymbol{x} = (x_1,\ldots ,x_n)\in X^n$, where $X$ is an Archimedean vector lattice and $n\in{\mathbb{N}}$: • there is a vector lattice homomorphism $\Phi _{\boldsymbol{x}}\colon H_n\to X$ such that $$\begin{equation*}\Phi_{\boldsymbol{x}}(\pi_i^{(n)}) = x_i\qquad (i\in\{1,\ldots,n\}),\end{equation*}$$where $H_n$ denotes the vector lattice of positively homogeneous, continuous, real-valued fu
APA, Harvard, Vancouver, ISO, and other styles
4

Sangiorgi, Davide, and Xian Xu. "Trees from Functions as Processes." Logical Methods in Computer Science Volume 14, Issue 3 (August 27, 2018). https://doi.org/10.23638/lmcs-14(3:11)2018.

Full text
Abstract:
Levy-Longo Trees and Bohm Trees are the best known tree structures on the {\lambda}-calculus. We give general conditions under which an encoding of the {\lambda}-calculus into the {\pi}-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the call-by-name {\lambda}-calculus, showing how the two kinds of tree can be obtained by varying the behavioural equivalence adopted in the {\pi}-calculus and/or the encoding.
APA, Harvard, Vancouver, ISO, and other styles
5

Hirschowitz, André, Tom Hirschowitz, and Ambroise Lafont. "Modules over monads and operational semantics (expanded version)." Logical Methods in Computer Science Volume 18, Issue 3 (August 2, 2022). http://dx.doi.org/10.46298/lmcs-18(3:3)2022.

Full text
Abstract:
This paper is a contribution to the search for efficient and high-level mathematical tools to specify and reason about (abstract) programming languages or calculi. Generalising the reduction monads of Ahrens et al., we introduce transition monads, thus covering new applications such as lambda-bar-mu-calculus, pi-calculus, Positive GSOS specifications, differential lambda-calculus, and the big-step, simply-typed, call-by-value lambda-calculus. Moreover, we design a suitable notion of signature for transition monads.
APA, Harvard, Vancouver, ISO, and other styles
6

Paulus, Joseph W. N., Daniele Nantes-Sobrinho, and Jorge A. Pérez. "Non-Deterministic Functions as Non-Deterministic Processes (Extended Version)." Logical Methods in Computer Science Volume 19, Issue 4 (October 10, 2023). http://dx.doi.org/10.46298/lmcs-19(4:1)2023.

Full text
Abstract:
We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambdafail, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider spi, a pi-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of lambdafail into spi and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-pr
APA, Harvard, Vancouver, ISO, and other styles
7

Madiot, Jean-Marie, Damien Pous, and Davide Sangiorgi. "Modular coinduction up-to for higher-order languages via first-order transition systems." Logical Methods in Computer Science Volume 17, Issue 3 (September 17, 2021). http://dx.doi.org/10.46298/lmcs-17(3:25)2021.

Full text
Abstract:
The bisimulation proof method can be enhanced by employing `bisimulations up-to' techniques. A comprehensive theory of such enhancements has been developed for first-order (i.e., CCS-like) labelled transition systems (LTSs) and bisimilarity, based on abstract fixed-point theory and compatible functions. We transport this theory onto languages whose bisimilarity and LTS go beyond those of first-order models. The approach consists in exhibiting fully abstract translations of the more sophisticated LTSs and bisimilarities onto the first-order ones. This allows us to reuse directly the large corpu
APA, Harvard, Vancouver, ISO, and other styles
8

Emmerson, Parker. "Cyclic Patterns of Pi : A Pattern We've All Been Searching." December 10, 2022. https://doi.org/10.5281/zenodo.7422783.

Full text
Abstract:
To detect patterns in the transcendental number pi, we can use the following formula : r{Ξ, Π, Ρ, Σ}{Θ,Λ,Μ,Ν}∞, ∞ ⊃ -1+⍵kxb.b2{κ,Θ,Λ,Μ,Ν}∞ {ω,Ξ,Π,Ρ,Σ}∞ &&μ{g} ,f,g,h,i,j⃝⇈<Ω ⍺ a,b,c,d,e⃝⇈ σ[{υ, φ, χ, ψ}, {ω, Ξ, Π, Ρ, Σ}∞]∞ This formula uses the notion of subsets, the Greek letters Ξ, Π, Ρ, Σ and Θ, Λ, Μ, Ν to calculate the sum of the transcendental number pi over an
APA, Harvard, Vancouver, ISO, and other styles
9

Quaglia, Paola. "On the Finitary Characterization of pi-Congruences." BRICS Report Series 4, no. 52 (1997). http://dx.doi.org/10.7146/brics.v4i52.19273.

Full text
Abstract:
Some alternative characterizations of late full congruences, either strong or weak, are presented. Those congruences are classically defined by requiring the corresponding ground bisimilarity under all name substitutions. <br />We first improve on those infinitary definitions by showing that congruences can be alternatively characterized in the pi-calculus by sticking to a finite<br />number of carefully identified substitutions, and hence, by resorting to only a finite number of ground bisimilarity checks.<br />Then we investigate the same issue in both the ground and the no
APA, Harvard, Vancouver, ISO, and other styles
10

Foster, Camaron. "V03 - Achefield Cosmology and Recursive Symbolic Intelligence." April 18, 2025. https://doi.org/10.5281/zenodo.15238490.

Full text
Abstract:
<strong>Achefield Cosmology</strong> <em>Glyphogenetic Autopoiesis and the Birth of Zeta‑Recursive Symbolic Intelligence</em> <em>A Torsion-Based Model of Meaning Emergence in Recursive Symbolic Fields</em> &nbsp;This work extends glyphic intelligence into a cosmological regime, formalizing <strong>zeta-recursive glyphogenesis</strong> as a unifying driver of symbolic, physical, and ethical dynamics. <strong>Core Construct</strong> Zeta-recursive duality couples a glyph&rsquo;s <strong>achefield potential</strong> &Gamma;(𝒜, m) with its <strong>tension gradient</strong> &Xi;(𝒜, m) = &part;&Gam
APA, Harvard, Vancouver, ISO, and other styles
More sources

Dissertations / Theses on the topic "Lambda-Pi calculus"

1

Hondet, Gabriel. "Expressing predicate subtyping in computational logical frameworks." Electronic Thesis or Diss., université Paris-Saclay, 2022. http://www.theses.fr/2022UPASG070.

Full text
Abstract:
Le typage permet d'apporter de la sûreté dans la programmation, et il est utilisé au coeur de la majorité des systèmes de preuve. Plus un système de types est expressif, plus il est aisé d'y encoder des invariantsqui seront vérifiés mécaniquement lors du typage. Les types dépendants sont une extension des types simples dans laquelle les types peuvent dépendre de valeurs. Ils permettent par exemple de définir les vecteurs paramétrés par leur longueur. Le sous-typage par prédicat est une autre extension des types simples, dans laquelle les types peuvent être définis par des prédicats. Un sous-ty
APA, Harvard, Vancouver, ISO, and other styles
2

ABDICHE, MINA. "Pi-calcul et sous-typage : inference de types et codages du lambda-calcul dans le pi-calcul." Paris 11, 2000. http://www.theses.fr/2000PA112214.

Full text
Abstract:
Le pi-calcul est une algebre de processus definie a partir de deux concepts : nommer et communiquer. Les noms sont des canaux de communication, et communiquer consiste a echanger des noms. Le pi-calcul permet ainsi de representer des systemes concurrents dont les liens de communication peuvent evoluer dynamiquement. Le pi-calcul possede une grande puissance d'expression. On peut y coder diverses structures de donnees. Il permet de retrouver toute la puissance d'expression du lambda-calcul vu qu'on peut y coder ce dernier. On peut aussi y representer des objets et des objets concurrents ainsi q
APA, Harvard, Vancouver, ISO, and other styles
3

Saillard, Ronan. "Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique." Thesis, Paris, ENMP, 2015. http://www.theses.fr/2015ENMP0027/document.

Full text
Abstract:
La vérification automatique de preuves consiste à faire vérifier par un ordinateur la validité de démonstrations d'énoncés mathématiques. Cette vérification étant purement calculatoire, elle offre un haut degré de confiance. Elle est donc particulièrement utile pour vérifier qu'un logiciel critique, c'est-à-dire dont le bon fonctionnement a un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens, correspond exactement à sa spécification. DEDUKTI est l'un de ces vérificateurs de preuves. Il implémente un système de type, le lambda-Pi-Calcul Modulo, qui est une
APA, Harvard, Vancouver, ISO, and other styles
4

Beffara, Emmanuel. "Logique, Réalisabilité et Concurrence." Phd thesis, Université Paris-Diderot - Paris VII, 2005. http://tel.archives-ouvertes.fr/tel-00011205.

Full text
Abstract:
Cette thèse se consacre à l'application de techniques de réalisabilité dans le cadre de l'étude du sens calculatoire de la logique. Dans une première partie, nous rappelons le formalisme de la réalisabilité classique de Krivine, dans lequel nous menons ensuite une étude du contenu opérationnel de tautologies purement classiques. Cette exploration du sens calculatoire de la disjonction classique révèle des comportements riches, avec une forte intuition interactive, qui s'interprètent avantageusement comme des structures de contrôle typées. Afin de mieux comprendre la nature de ces mécanismes, n
APA, Harvard, Vancouver, ISO, and other styles
5

Laurent, Olivier. "Investigations classiques, complexes et concurrentes à l'aide de la logique linéaire." Habilitation à diriger des recherches, Université Paris-Diderot - Paris VII, 2010. http://tel.archives-ouvertes.fr/tel-00460805.

Full text
Abstract:
La logique linéaire fait désormais partie des outils standards en théorie de la démonstration et, de manière plus générale, dans l'étude de la correspondance de Curry-Howard. Nous présentons ici trois directions importantes d'application de méthodes issues de la logique linéaire : - la théorie de la démonstration de la logique classique et ses aspects calculatoires via notamment la sémantique des jeux ; - la complexité implicite à travers les modèles dénotationnels des logiques linéaires à complexité bornée ; - la théorie de la concurrence et ses fondements logiques grâce aux ingrédients appor
APA, Harvard, Vancouver, ISO, and other styles

Book chapters on the topic "Lambda-Pi calculus"

1

Cousineau, Denis, and Gilles Dowek. "Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo." In Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2007. http://dx.doi.org/10.1007/978-3-540-73228-0_9.

Full text
APA, Harvard, Vancouver, ISO, and other styles
2

Kuttler, Céline, and Joachim Niehren. "Gene Regulation in the Pi Calculus: Simulating Cooperativity at the Lambda Switch." In Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2006. http://dx.doi.org/10.1007/11905455_2.

Full text
APA, Harvard, Vancouver, ISO, and other styles

Conference papers on the topic "Lambda-Pi calculus"

1

Färber, Michael. "Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting." In CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, 2022. http://dx.doi.org/10.1145/3497775.3503683.

Full text
APA, Harvard, Vancouver, ISO, and other styles
2

Intrigila, B., and R. Statman. "The omega rule is /spl Pi//sub 2//sup 0/-hard in the /spl lambda//spl beta/-calculus." In Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004. IEEE, 2004. http://dx.doi.org/10.1109/lics.2004.1319614.

Full text
APA, Harvard, Vancouver, ISO, and other styles
You might also be interested in the extended bibliographies on the topic 'Lambda-Pi calculus' for particular source types:
Journal articles
We offer discounts on all premium plans for authors whose works are included in thematic literature selections. Contact us to get a unique promo code!

To the bibliography